proposition: Theorem iter_succ_r : forall p (A:Type) (f:A -> A) (x:A), iter f x (succ p) = iter f (f x) p.
proof: Proof. intros; now rewrite iter_succ, iter_swap. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef