proposition: Lemma power_series_sum : forall H Hc, series_sum (power_series c) Hc [=] ([1][/] [1][-]c[//]H).
proof: Proof. intros. unfold series_sum in |- *. apply eq_symmetric_unfolded; apply Limits_unique. apply power_series_Lim1. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)