Moessner's Theorem: an extensive exercise in coinduction

We use coinduction to give new proofs of the theorems by Moessner (1951)
and Paasche (1952), which are two non-trivial and entertaining
combinatorial observations on infinite sequences (streams) of natural
numbers. As we shall see, the heart of the matter in this coinductive
approach is the identification of the circularity in the streams at
hand, which leads to surprisingly simple end elementary proofs. A key
ingredient in exposing this circularity is the combined use of algebraic
and coalgebraic structure.