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/complex/AbsCC".
19 (* $Id: AbsCC.v,v 1.2 2004/04/23 10:00:54 lcf Exp $ *)
25 (*#* * Absolute value on [CC]
26 ** Properties of [AbsCC] *)
29 Section AbsCC_properties.
32 inline cic:/CoRN/complex/AbsCC/AbsCC_nonneg.con.
34 inline cic:/CoRN/complex/AbsCC/AbsCC_ap_zero_imp_pos.con.
36 inline cic:/CoRN/complex/AbsCC/AbsCC_wd.con.
39 Hint Resolve AbsCC_wd: algebra_c.
42 inline cic:/CoRN/complex/AbsCC/cc_inv_abs.con.
45 Hint Resolve cc_inv_abs: algebra.
48 inline cic:/CoRN/complex/AbsCC/cc_minus_abs.con.
50 inline cic:/CoRN/complex/AbsCC/cc_mult_abs.con.
53 Hint Resolve cc_mult_abs: algebra.
56 inline cic:/CoRN/complex/AbsCC/AbsCC_minzero.con.
58 inline cic:/CoRN/complex/AbsCC/AbsCC_IR.con.
61 Hint Resolve AbsCC_IR: algebra.
64 inline cic:/CoRN/complex/AbsCC/cc_div_abs.con.
66 inline cic:/CoRN/complex/AbsCC/cc_div_abs'.con.
68 inline cic:/CoRN/complex/AbsCC/AbsCC_zero.con.
71 Hint Resolve AbsCC_zero: algebra.
74 inline cic:/CoRN/complex/AbsCC/AbsCC_one.con.
76 inline cic:/CoRN/complex/AbsCC/cc_pow_abs.con.
78 inline cic:/CoRN/complex/AbsCC/AbsCC_pos.con.
80 inline cic:/CoRN/complex/AbsCC/AbsCC_ap_zero.con.
82 inline cic:/CoRN/complex/AbsCC/AbsCC_small_imp_eq.con.
86 inline cic:/CoRN/complex/AbsCC/l_1_1_2.con.
91 Hint Resolve l_1_1_2: algebra.
94 inline cic:/CoRN/complex/AbsCC/AbsCC_square_Re_Im.con.
97 Hint Resolve AbsCC_square_Re_Im: algebra.
102 inline cic:/CoRN/complex/AbsCC/l_1_2_3_CC.con.
107 Hint Resolve l_1_2_3_CC: algebra.
110 inline cic:/CoRN/complex/AbsCC/AbsCC_mult_conj.con.
113 Hint Resolve CC_conj_mult: algebra.
118 inline cic:/CoRN/complex/AbsCC/l_2_1_2.con.
121 Hint Resolve l_2_1_2: algebra.
126 inline cic:/CoRN/complex/AbsCC/AbsCC_mult_square.con.
128 inline cic:/CoRN/complex/AbsCC/AbsCC_square_ap_zero.con.
130 inline cic:/CoRN/complex/AbsCC/cc_recip_char.con.
132 inline cic:/CoRN/complex/AbsCC/AbsCC_strext.con.
134 inline cic:/CoRN/complex/AbsCC/AbsSmallCC.con.
136 inline cic:/CoRN/complex/AbsCC/Cexis_AFS_CC.con.
138 (* The following lemmas are just auxiliary results *)
142 inline cic:/CoRN/complex/AbsCC/l_4_1_2.con.
144 inline cic:/CoRN/complex/AbsCC/l_4_2_3.con.
146 inline cic:/CoRN/complex/AbsCC/l_4_3_4.con.
151 End AbsCC_properties.
155 Hint Resolve AbsCC_wd: algebra_c.
159 Hint Resolve cc_inv_abs cc_mult_abs cc_div_abs cc_div_abs' cc_pow_abs
160 AbsCC_zero AbsCC_one AbsCC_IR AbsCC_mult_conj AbsCC_mult_square
161 cc_recip_char: algebra.
164 (*#* ** The triangle inequality *)
166 inline cic:/CoRN/complex/AbsCC/triangle.con.
168 inline cic:/CoRN/complex/AbsCC/triangle_Sum.con.