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 a. induction n as [|n Hn]. - reflexivity. - simpl. rewrite H, Hn. reflexivity. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass