proposition: Lemma gt_abs_pser_unfold : forall An r, gt_abs_pser An r == gt_pser (| An |) (Rabs r).
proof: Proof. intros An r n ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult ; rewrite RPow_abs ; apply Rabs_mult. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def