proposition: Lemma gt_abs_pser_1 : forall An n, gt_abs_pser An 1 n = Rabs (An n).
proof: Proof. intros An n ; unfold gt_abs_pser, Rseq_abs ; f_equal ; apply gt_pser_1. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def