proposition: Lemma iter_addR x (n : nat) : ssrnat.iter n (Rplus x) 0 = n%:R * x.
proof: Proof. by rewrite iter_addr addr0 -mulr_natr mulrC RmultE INRE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)