proposition: Lemma finite_cv_radius_scal_compat : forall (An : Rseq) (lam r : R), lam <> 0 -> (finite_cv_radius An r <-> finite_cv_radius (lam * An)%Rseq r).
proof: Proof. intros An lam r lam_neq ; split ; intros [H_inf H_sup]. split ; intros r' ; rewrite <- Cv_radius_weak_scal ; [apply H_inf | | apply H_sup |] ; assumption. split ; intros r' ; rewrite (Cv_radius_weak_scal _ lam) ; [apply H_inf | | apply H_sup |] ; assumption. 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