proposition: Lemma Sum0_c_exp : forall H m, Sum0 m (fun i => c[^]i) [=] (c[^]m[-][1][/] c[-][1][//]H).
proof: Proof. intros. elim m. simpl in |- *. rational. simpl in |- *. intros. astepl ((nexp IR n c[-][1][/] c[-][1][//]H) [+]nexp IR n c). rational. Qed.
imports: CoRN.reals.CReals1