proposition: Lemma iterateN_f : forall A f (z:A) n, iterateN f (f z) n = map f (iterateN f z n).
proof: Proof. intros A f z n. revert f z. induction n. reflexivity. simpl. intros f z. rewrite <- IHn. reflexivity. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid