Church numeral (rocq)

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

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