proposition: Lemma iter_rect (A:Type) (f:A -> A) (a:A) (P:nat -> A -> Type) : P 0 a -> (forall n a', P n a' -> P (S n) (f a')) -> forall n, P n (iter n f a).
proof: Proof. intros H0 HS n. induction n as [|n Hn]. - exact H0. - apply HS. exact Hn. Defined.
imports: NAxioms NProperties OrdersFacts DecidableClass