proposition: Lemma Rseq_pps_alt_compat : forall An x, Rseq_pps (Rseq_alt An) x == Rseq_pps An (- x).
proof: Proof. intros An x n ; induction n. do 2 rewrite Rseq_pps_O_simpl ; unfold Rseq_alt, Rseq_mult, Rseq_pow ; apply Rmult_1_l. do 2 rewrite Rseq_pps_simpl ; rewrite IHn ; apply Rplus_eq_compat_l. unfold Rseq_alt, Rseq_mult, Rseq_pow ; rewrite (unfold_Ropp x), Rpow_mult_distr ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra