proposition: Lemma gt_pser_0 : forall An r, gt_pser An r O = An O.
proof: Proof. intros ; unfold gt_pser, Rseq_mult ; rewrite pow_O ; apply Rmult_1_r. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def