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