proposition: Lemma sum_n_m_mult_l : forall (a : K) (u : nat -> K) (n m : nat), sum_n_m (fun k => mult a (u k)) n m = mult a (sum_n_m u n m).
proof: Proof. intros a u n m. case: (le_dec n m) => Hnm. elim: m n u Hnm => [ | m IH] n u Hnm. apply Nat.le_0_r in Hnm. by rewrite -Hnm !sum_n_n. destruct n. rewrite !sum_n_Sm ; try by apply Nat.le_0_l. rewrite IH. by apply sym_eq, mult_distr_l. by apply Nat.le_0_l. rewrite -!sum_n_m_S. apply IH. by apply le_S_n. apply not_le in Hnm. rewrite !sum_n_m_zero //. by rewrite mult_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub