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