proposition: Lemma Sum_c_exp' : forall H m n, Sum m n (fun i => c[^]i) [=] (c[^]m[-]c[^]S n[/] [1][-]c[//]H).
proof: Proof. intros. cut (c[-][1] [#] [0]). intro H0. astepl (c[^]S n[-]c[^]m[/] c[-][1][//]H0). rational. rstepl ( [--] ([1][-]c)). apply inv_resp_ap_zero. assumption. Qed.
imports: CoRN.reals.CReals1