proposition: Lemma Rseq_sum_minus_compat : forall Un Vn, Rseq_sum (Un - Vn) == Rseq_sum Un - Rseq_sum Vn.
proof: Proof. intros Un Vn n ; rewrite Rseq_sum_ext with (Un - Vn) (Un + (- Vn)) _, Rseq_sum_plus_compat. unfold Rseq_plus, Rseq_minus ; rewrite Rseq_sum_opp_compat ; reflexivity. unfold Rseq_minus ; intro ; reflexivity. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra