proposition: Lemma sum_n_scal_l : forall (a : K) (u : nat -> V) (n : nat), sum_n (fun k => scal a (u k)) n = scal a (sum_n u n).
proof: Proof. intros a u n. apply sum_n_m_scal_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub