(* 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.