proposition: Lemma Rseq_sum_plus_compat : forall Un Vn, Rseq_sum (Un + Vn) == Rseq_sum Un + Rseq_sum Vn.
proof: Proof. intros Un Vn n ; induction n. reflexivity. simpl ; rewrite IHn ; unfold Rseq_plus ; simpl ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra