proposition: Lemma iter_const {I} (l : list I) (a : R) : iter Rplus 0 l (fun _ => a) = INR (length l) * a.
proof: Proof. elim: l => /= [ | h l ->]. by rewrite /= Rmult_0_l. case: (length l) => [ | n] ; simpl ; ring. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements