proposition: Theorem iter_ind (A:Type) (f:A -> A) (a:A) (P:N -> A -> Prop) : P 0 a -> (forall n a', P n a' -> P (succ n) (f a')) -> forall n, P n (iter n f a).
proof: Proof. intros ? ? n; induction n using peano_ind; trivial. rewrite iter_succ; auto. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties