proposition: Lemma Rseq_sum_lt_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_lt_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