proposition: Lemma Rseq_pps_plus_compat : forall An Bn x, Rseq_pps (An + Bn) x == Rseq_pps An x + Rseq_pps Bn x.
proof: Proof. intros An Bn x n ; unfold Rseq_pps ; rewrite Rseq_sum_ext with _ ((An * (pow x)) + (Bn * (pow x))) _. apply Rseq_sum_plus_compat. clear ; intro n ; unfold gt_pser, Rseq_mult, Rseq_plus ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra