proposition: Theorem iter_add : forall p q (A:Type) (f:A -> A) (x:A), iter f x (p+q) = iter f (iter f x q) p.
proof: Proof. intro p; induction p as [|p IHp] using peano_ind; intros. - now rewrite add_1_l, iter_succ. - now rewrite add_succ_l, !iter_succ, IHp. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef