proposition: Lemma gt_abs_pser_le_compat : forall An r r' n, Rabs r <= Rabs r' -> gt_abs_pser An r n <= gt_abs_pser An r' n.
proof: Proof. intros An r r' n Hrr' ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult ; do 2 rewrite Rabs_mult, <- RPow_abs ; apply Rmult_le_compat_l ; [apply Rabs_pos |] ; apply pow_le_compat ; [apply Rabs_pos | assumption]. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def