proposition: Lemma Rseq_bound_plus : Rseq_bound (Un + Vn) (lu + lv).
proof: Proof. intro n ; unfold Rseq_plus ; apply Rle_trans with (Rabs (Un n) + Rabs (Vn n))%R ; [apply Rabs_triang | apply Rplus_le_compat ; auto]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_sums_facts Rsequence_rewrite_facts Lra MyRIneq