proposition: Lemma Rseq_sum_le_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 Hle ; induction n. simpl ; apply Hle ; trivial. simpl ; transitivity (Rseq_sum Bn n + An (S n))%R. apply Rplus_le_compat_r ; apply IHn ; auto. apply Rplus_le_compat_l ; apply Hle ; trivial. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra