proposition: Lemma Rseq_sum_ext : forall Un Vn, Un == Vn -> Rseq_sum Un == Rseq_sum Vn.
proof: Proof. intros Un Vn Heq n ; apply Rseq_sum_ext_strong ; trivial. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra