proposition: Lemma iter_cat l1 l2 f : iter (l1 ++ l2) f = op (iter l1 f) (iter l2 f).
proof: Proof. elim: l1 => [ | h1 l1 IH] /=. by rewrite neutral_l. by rewrite IH assoc. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements