include "ground/arith/nat_iter.ma".
include "ground/arith/nat_succ.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
-(* Rewrites with niter ******************************************************)
+(* Constructions with niter *************************************************)
-lemma niter_succ (A) (f) (n) (a): f (f^n a) = f^{A}(↑n) a.
+(*** iter_S *)
+lemma niter_succ (A) (f) (n): f ∘ f^n ≐ f^{A}(↑n).
#A #f * //
qed.