include "ground/arith/pnat_iter.ma".
include "ground/arith/nat.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ITERATED FUNCTION FOR NON-NEGATIVE INTEGERS ******************************)
definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
match n with