proposition: Lemma Rpser_abs_unfold : forall An r l, Rpser_abs An r l <-> Rpser (| An |) (Rabs r) l.
proof: Proof. intros An r l ; split ; intro Hyp ; unfold Rpser, Rpser_abs ; assert (tmp := Rseq_pps_abs_unfold An r) ; eapply Rseq_cv_eq_compat ; eauto ; symmetry ; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra