Church numeral rocq

Church's encoding of numbers used in Pure/Untyped lambda calculus.

Encoding: $c_n = \lambda a.\ \lambda z.\ \underbrace{a\ (a\ (\cdots (a}_{n}\ z)\cdots))$.