proposition: Lemma Rpser_expand_compat : forall An l x la, Rpser An (l * x) la -> Rpser (An_expand An l) x la.
proof: Proof. intros ; eapply Rseq_cv_eq_compat. eapply Rseq_sum_ext ; intro ; apply gt_pser_expand_compat. assumption. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR