proposition: Lemma Rseq_pps_simpl : forall An x n, Rseq_pps An x (S n) = (Rseq_pps An x n + (An (S n) * pow x (S n)))%R.
proof: Proof. intros ; reflexivity. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra