proposition: Theorem iter_add : forall p q (A:Type) (f:A -> A) (x:A), iter (p+q) f x = iter p f (iter q f x).
proof: Proof. intro p; induction p as [|p IHp] using peano_ind; intros; trivial. now rewrite add_succ_l, !iter_succ, IHp. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties