proposition: Lemma Rseq_pps_ext : forall An Bn x, (An == Bn)%Rseq -> (Rseq_pps An x == Rseq_pps Bn x)%Rseq.
proof: Proof. intros An Bn x Hext ; apply Rseq_sum_ext ; intro n ; unfold gt_pser, Rseq_mult ; rewrite Hext ; reflexivity. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra