proposition: Lemma conv_series_mult_scal : convergent (fun n => c[*]x n).
proof: Proof. red in |- *. red in convX. eapply Cauchy_prop_wd. apply Cauchy_mult with (seq2 := Build_CauchySeq _ _ convX) (seq1 := Cauchy_const c). simpl in |- *. unfold seq_part_sum in |- *. intro. apply eq_symmetric_unfolded. apply Sum0_comm_scal'. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)