proposition: Lemma Rseq_sum_le_compat: forall An Bn n, (forall n, An n <= Bn n) -> Rseq_sum An n <= Rseq_sum Bn n.
proof: Proof. intros ; apply Rseq_sum_le_compat_strong ; trivial. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra