proposition: Lemma Rseq_pps_scal_compat_l : forall (l : R) An x, (Rseq_pps (l * An) x == l * Rseq_pps An x)%Rseq.
proof: Proof. intros l An x n ; unfold Rseq_pps ; rewrite Rseq_sum_ext with _ (l * (An * (pow x)))%Rseq _. apply Rseq_sum_scal_compat_l. 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