proposition: Lemma Rseq_pps_opp_compat : forall An x, (Rseq_pps (- An) x == - Rseq_pps An x)%Rseq.
proof: Proof. intros An x n ; unfold Rseq_pps ; rewrite Rseq_sum_ext with _ (- (An * (pow x))) _. apply Rseq_sum_opp_compat. clear ; intro n ; unfold gt_pser, Rseq_mult, Rseq_opp ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra