proposition: Lemma series_sum_mult_scal : forall H : convergent (fun n => c[*]x n), series_sum _ H [=] c[*]series_sum _ convX.
proof: Proof. intros. unfold series_sum in |- *. apply eq_transitive_unfolded with (Lim (Cauchy_const c) [*]Lim (Build_CauchySeq _ _ convX)). 2: apply mult_wdl; apply eq_symmetric_unfolded; apply Lim_const. eapply eq_transitive_unfolded. 2: apply Lim_mult. apply Lim_wd'. intro; simpl in |- *. unfold seq_part_sum in |- *. apply Sum0_comm_scal'. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)