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