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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/CSumsReals".
19 (* $Id: CSumsReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
25 (*#* * Sums over Reals
27 %\begin{convention}% Let [c] be a real.
31 $\Sigma_{m\leq i \leq n}~c^k = \frac{c^{n+1}-c^m}{c-1}.$
32 #sum_(m≤ i ≤ n) c^k = frac (c^(n+1) -c^m) (c-1)#
36 Section Sums_over_Reals.
39 inline cic:/CoRN/reals/CSumsReals/c.var.
41 inline cic:/CoRN/reals/CSumsReals/Sum0_c_exp.con.
44 Hint Resolve Sum0_c_exp.
47 inline cic:/CoRN/reals/CSumsReals/Sum_c_exp.con.
50 Hint Resolve Sum_c_exp.
53 (*#* The following formulation is often more useful if [c [<] 1]. *)
55 inline cic:/CoRN/reals/CSumsReals/Sum_c_exp'.con.
58 Hint Resolve Sum_c_exp'.
66 Hint Resolve Sum0_c_exp Sum_c_exp Sum_c_exp': algebra.
69 inline cic:/CoRN/reals/CSumsReals/diff_is_Sum0.con.
71 inline cic:/CoRN/reals/CSumsReals/diff_is_sum.con.
73 inline cic:/CoRN/reals/CSumsReals/Sum0_pres_less.con.
75 inline cic:/CoRN/reals/CSumsReals/Sum_pres_less.con.
77 inline cic:/CoRN/reals/CSumsReals/Sum_pres_leEq.con.
79 inline cic:/CoRN/reals/CSumsReals/Sum0_comm_scal.con.
82 Hint Resolve Sum0_comm_scal: algebra.
85 inline cic:/CoRN/reals/CSumsReals/Sum_comm_scal.con.
87 inline cic:/CoRN/reals/CSumsReals/Sum0_comm_scal'.con.
89 inline cic:/CoRN/reals/CSumsReals/Sum_comm_scal'.con.
91 inline cic:/CoRN/reals/CSumsReals/Sumx_comm_scal'.con.
93 inline cic:/CoRN/reals/CSumsReals/Sum2_comm_scal'.con.