proposition: Lemma gt_abs_pser_0_ub : forall An n, gt_abs_pser An 0 n <= Rabs (An O).
proof: Proof. intros An [ |i] ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult. rewrite pow_O, Rmult_1_r ; reflexivity. rewrite pow_i ; [rewrite Rmult_0_r, Rabs_R0 ; apply Rabs_pos | lia]. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def