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".
21 (* $Id: CSumsReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
23 include "reals/CReals1.ma".
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 alias id "c" = "cic:/CoRN/reals/CSumsReals/Sums_over_Reals/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".