proposition: Lemma Rseq_pps_abs_unfold : forall An x, Rseq_pps_abs An x == Rseq_pps (| An |) (Rabs x).
proof: Proof. intros An x ; apply Rseq_sum_ext ; apply gt_abs_pser_unfold. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra