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