proposition: Lemma Rseq_sum_triang: forall An n, Rabs (Rseq_sum An n) <= Rseq_sum (| An |) n.
proof: Proof. intros An n ; induction n. unfold Rseq_abs ; simpl ; reflexivity. do 2 rewrite Rseq_sum_simpl ; eapply Rle_trans ; [eapply Rabs_triang |] ; apply Rplus_le_compat ; [assumption | reflexivity]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra