proposition: Theorem iter_succ : forall n (A:Type) (f:A -> A) (x:A), iter (succ n) f x = f (iter n f x).
proof: Proof. intro n; destruct n; intros; simpl; trivial. now apply Pos.iter_succ. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties