proposition: Lemma sum_n_mult_l : forall (a : K) (u : nat -> K) (n : nat), sum_n (fun k => mult a (u k)) n = mult a (sum_n u n).
proof: Proof. intros ; by apply sum_n_m_mult_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub