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