proposition: Lemma norm_sum_n_m {K : AbsRing} {V : NormedModule K} (a : nat -> V) (n m : nat) : norm (sum_n_m a n m) <= sum_n_m (fun n => norm (a n)) n m.
proof: Proof. case: (le_dec n m) => Hnm. elim: m n a Hnm => /= [ | m IH] n a Hnm. apply Nat.le_0_r in Hnm. rewrite -Hnm !sum_n_n. by apply Rle_refl. destruct n. rewrite /sum_n !sum_n_Sm ; try by apply Nat.le_0_l. eapply Rle_trans. apply norm_triangle. apply Rplus_le_compat_r, IH, 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 // norm_zero. by apply Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub