A characterization of Moessner's sieve

Given a positive natural number n  , Moessner's sieve constructs the stream of positive natural numbers exponentiated at that rank: 1n1n, 2n2n, 3n3n, etc., without performing any multiplications. Moessner's sieve starts from the stream of positive natural numbers, and proceeds iteratively: first it strikes out every n  th number and maps the result into a stream of partial sums; then it strikes out every (n−1)(n−1)th number and maps the result into a stream of partial sums; […]; then it strikes out every 3rd number and maps the result into a stream of partial sums; and then it strikes out every 2nd number and maps the result into a stream of partial sums. Moessner's theorem states that the end result of this sieve is the stream of positive natural numbers exponentiated at rank n. In this article, we generalize Moessner's sieve to rank 0, we formalize it with the Coq proof assistant, we present generating functions for the numbers that are struck out at each iteration, we define its left inverse, and we touch upon Long's theorem, which generalizes Moessner's theorem.Given a natural number n  , we characterize the successive streams of numbers that are struck out as enumerating the successive monomials of the binomial expansion of (1+x)n(1+x)n. To this end, we initialize Moessner's sieve with a stream that starts with 1 and continues with 0's, and we add a final step where we pick every number in the resulting stream. Since the last monomial is xnxn, Moessner's theorem at rank n follows as a corollary.