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 *************************************************)
+(*** iter_S *)
lemma niter_succ (A) (f) (n) (a): f (f^n a) = f^{A}(↑n) a.
#A #f * //
qed.