proposition: Lemma iter_comp (l : list I) f (g : I -> I) : iter l (fun x => f (g x)) = iter (map g l) f.
proof: Proof. elim: l => [ | s l IH] //=. by rewrite IH. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements