proposition: Lemma iter_swap_gen A B (f:A -> B) (g:A -> A) (h:B -> B) : (forall a, f (g a) = h (f a)) -> forall n a, f (iter n g a) = iter n h (f a).
proof: Proof. intros H n; destruct n; simpl; intros; rewrite ?H; trivial. now apply Pos.iter_swap_gen. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties