proposition: Lemma gt_pser_ext : forall An Bn x, An == Bn -> gt_pser An x == gt_pser Bn x.
proof: Proof. intros An Bn x Heq n ; unfold gt_pser, Rseq_mult ; rewrite Heq ; reflexivity. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def