An exercise in coinduction: Moessner's theorem

We present a coinductive proof of Moessner’s theorem. This theorem describes the construction of the stream (1^n,2^n,3^, ...) (for n > 0) out of the stream of natural numbers by repeatedly dropping and summing elements. Our formalisation consists of a direct translation of the operational description of Moessner’s procedure into the equivalence of - in essence - two functional programs. Our proof fully exploits the circularity that is present in Moessner’s procedure and is more elementary than existing proofs. As such, it serves as a non-trivial illustration of the relevance and power of coinduction.