proposition: Lemma Rseq_pps_O_simpl : forall An x, Rseq_pps An x O = An O.
proof: Proof. intros An x ; unfold Rseq_pps ; apply gt_pser_0. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra