1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: CSumsReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
21 include "reals/CReals1.ma".
23 (*#* * Sums over Reals
25 %\begin{convention}% Let [c] be a real.
29 $\Sigma_{m\leq i \leq n}~c^k = \frac{c^{n+1}-c^m}{c-1}.$
30 #sum_(m≤ i ≤ n) c^k = frac (c^(n+1) -c^m) (c-1)#
34 Section Sums_over_Reals
38 cic:/CoRN/reals/CSumsReals/Sums_over_Reals/c.var
41 inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_c_exp.con" as lemma.
44 Hint Resolve Sum0_c_exp.
47 inline procedural "cic:/CoRN/reals/CSumsReals/Sum_c_exp.con" as lemma.
50 Hint Resolve Sum_c_exp.
53 (*#* The following formulation is often more useful if [c [<] 1]. *)
55 inline procedural "cic:/CoRN/reals/CSumsReals/Sum_c_exp'.con" as lemma.
58 Hint Resolve Sum_c_exp'.
66 Hint Resolve Sum0_c_exp Sum_c_exp Sum_c_exp': algebra.
69 inline procedural "cic:/CoRN/reals/CSumsReals/diff_is_Sum0.con" as lemma.
71 inline procedural "cic:/CoRN/reals/CSumsReals/diff_is_sum.con" as lemma.
73 inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_pres_less.con" as lemma.
75 inline procedural "cic:/CoRN/reals/CSumsReals/Sum_pres_less.con" as lemma.
77 inline procedural "cic:/CoRN/reals/CSumsReals/Sum_pres_leEq.con" as lemma.
79 inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_comm_scal.con" as lemma.
82 Hint Resolve Sum0_comm_scal: algebra.
85 inline procedural "cic:/CoRN/reals/CSumsReals/Sum_comm_scal.con" as lemma.
87 inline procedural "cic:/CoRN/reals/CSumsReals/Sum0_comm_scal'.con" as lemma.
89 inline procedural "cic:/CoRN/reals/CSumsReals/Sum_comm_scal'.con" as lemma.
91 inline procedural "cic:/CoRN/reals/CSumsReals/Sumx_comm_scal'.con" as lemma.
93 inline procedural "cic:/CoRN/reals/CSumsReals/Sum2_comm_scal'.con" as lemma.