proposition: Lemma iterate_Sr {A} (f : A -> A) n a : iterate f (S n) a = iterate f n (f a).
proof: Proof. revert a; induction n. reflexivity. intros a. rewrite !iterate_S, <- IHn. reflexivity. Qed.
imports: Coq.Program.Tactics Coq.Arith.PeanoNat List FunctionalExtensionality