proposition: Lemma gt_abs_pser_scal_compat_r : forall Un (l : R) x, forall n, gt_abs_pser (Un * l) x n = gt_abs_pser Un x n * Rabs l.
proof: Proof. intros Un l x n ; unfold gt_abs_pser, Rseq_abs ; rewrite gt_pser_scal_compat_r ; apply Rabs_mult. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR