The specific definition of $\mathsf{succ}$ for Church numerals
$$ \mathsf{succ} = \lambda n f x. f (n f x) $$
seems to have an interesting property when applied to itself: (here, all expressions on $n$ mean the Church numeral that represents the value expressed by the value of $n$)
$$ \begin{align} \mathsf{succ} \; \mathsf{succ} \; n f x &= (n^2+n) f x \\ \mathsf{succ} \; \mathsf{succ} \; \mathsf{succ} \; n f x &= (n^2+n+1) f x \\ \mathsf{succ} \; \mathsf{succ} \; \mathsf{succ} \; \mathsf{succ} \; n f x &= (n^3+n^2+n) f x \\ \mathsf{succ} \; \mathsf{succ} \; \mathsf{succ} \; \mathsf{succ} \; \mathsf{succ} \; n f x &= (n^3+n^2+n+1) f x \end{align} $$
More generally these formulas hold:
$$ \begin{align} \underbrace{\mathsf{succ} \; \cdots \; \mathsf{succ}}_{2k \text{ times}} \; n f x &= (\sum_{i=1}^{k+1}{n^i}) f x \\ \underbrace{\mathsf{succ} \; \cdots \; \mathsf{succ}}_{2k+1 \text{ times}} \; n f x &= (\sum_{i=0}^{k+1}{n^i}) f x \end{align} $$
A proof attempt is here.
Now, imagine more general LC terms made of $\mathsf{succ}$s, such as $\mathsf{succ} (\mathsf{succ} \; \mathsf{succ})$, $\mathsf{succ} (\mathsf{succ} (\mathsf{succ} \; \mathsf{succ}) \mathsf{succ})$, etc. Are these polynomial functions on Church numerals as well? I once did some experiments, and more recently wrote a Mathematica program that "evaluates" such expressions via term rewriting, but I'm yet to find a rigorous proof that this holds for all such terms, or a proven counterexample. I can't even imagine where to start.