proposition: Lemma gt_abs_pser_S : forall An r n, gt_abs_pser An r (S n) = gt_abs_pser (Rseq_shift An) r n * Rabs r.
proof: Proof. intros An r n ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult, Rseq_shift ; simpl ; rewrite (Rmult_comm r), <- Rmult_assoc; apply Rabs_mult. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def