proposition: Lemma Rseq_sum_lt_compat_strong: forall An Bn n, (forall p, (p <= n)%nat -> An p < Bn p) -> Rseq_sum An n < Rseq_sum Bn n.
proof: Proof. intros An Bn n Hlt ; induction n. simpl ; apply Hlt ; trivial. simpl ; transitivity (Rseq_sum Bn n + An (S n))%R. apply Rplus_lt_compat_r ; apply IHn ; auto. apply Rplus_lt_compat_l ; apply Hlt ; trivial. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra