proposition: Lemma Cv_radius_weak_scal : forall (An : Rseq) (lambda r : R), lambda <> 0 -> (Cv_radius_weak An r <-> Cv_radius_weak (lambda * An)%Rseq r).
proof: Proof. intros An lam r lam_neq ; split ; intros [B HB] ; [exists (Rabs lam * B) | exists (B * / (Rabs lam))] ; intros x [n Hn] ; subst ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult. do 2 rewrite Rabs_mult ; rewrite Rmult_assoc ; apply Rmult_le_compat_l ; [apply Rabs_pos |] ; rewrite <- Rabs_mult ; apply HB ; exists n ; reflexivity. apply Rle_trans with (Rabs lam * Rabs (An n * r ^ n) * / Rabs lam) ; [right ; field ; apply Rabs_no_R0 ; assumption |]. rewrite <- Rabs_mult ; apply Rmult_le_compat_r ; [left ; apply Rinv_0_lt_compat ; apply Rabs_pos_lt ; assumption |]. rewrite <- Rmult_assoc ; apply HB ; exists n ; reflexivity. 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