proposition: Lemma Sum_c_exp : forall H m n, Sum m n (fun i => c[^]i) [=] (c[^]S n[-]c[^]m[/] c[-][1][//]H).
proof: Proof. intros. unfold Sum in |- *. unfold Sum1 in |- *. astepl ((c[^]S n[-][1][/] c[-][1][//]H) [-] (c[^]m[-][1][/] c[-][1][//]H)). rational. Qed.
imports: CoRN.reals.CReals1