proposition: Lemma gt_abs_pser_0 : forall An r, gt_abs_pser An r O = Rabs (An O).
proof: Proof. intros ; unfold gt_abs_pser, Rseq_abs ; rewrite gt_pser_0 ; reflexivity. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def