proposition: Lemma Rseq_pps_0_simpl : forall An n, Rseq_pps An 0 n = An O.
proof: Proof. intros An n ; induction n. unfold Rseq_pps, gt_pser, Rseq_mult ; simpl ; rewrite Rmult_1_r ; reflexivity. rewrite Rseq_pps_simpl, IHn, pow_i ; [ring | lia]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra