proposition: Lemma sum_n_m_le (a b : nat -> R) (n m : nat) : (forall k, a k <= b k) -> sum_n_m a n m <= sum_n_m b n m.
proof: Proof. intros H. case: (le_dec n m) => Hnm. elim: m n a b Hnm H => /= [ | m IH] n a b Hnm H. apply Nat.le_0_r in Hnm ; rewrite -Hnm. rewrite !sum_n_n ; by apply H. destruct n. rewrite !sum_n_Sm ; try by apply Nat.le_0_l. apply Rplus_le_compat. apply IH => // ; by apply Nat.le_0_l. by apply H. rewrite -!sum_n_m_S. apply IH => //. by apply le_S_n. apply not_le in Hnm. rewrite !sum_n_m_zero //. by apply Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub