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