proposition: Lemma gt_abs_pser_ext : forall An Bn x, An == Bn -> gt_abs_pser An x == gt_abs_pser Bn x.
proof: Proof. intros ; intro n ; unfold gt_abs_pser, Rseq_abs ; erewrite gt_pser_ext ; eauto. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def