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: AbsCC.v,v 1.2 2004/04/23 10:00:54 lcf Exp $ *)
21 include "complex/CComplex.ma".
23 (*#* * Absolute value on [CC]
24 ** Properties of [AbsCC] *)
27 Section AbsCC_properties
30 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_nonneg.con".
32 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_ap_zero_imp_pos.con".
34 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_wd.con".
37 Hint Resolve AbsCC_wd: algebra_c.
40 inline procedural "cic:/CoRN/complex/AbsCC/cc_inv_abs.con".
43 Hint Resolve cc_inv_abs: algebra.
46 inline procedural "cic:/CoRN/complex/AbsCC/cc_minus_abs.con".
48 inline procedural "cic:/CoRN/complex/AbsCC/cc_mult_abs.con".
51 Hint Resolve cc_mult_abs: algebra.
54 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_minzero.con".
56 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_IR.con".
59 Hint Resolve AbsCC_IR: algebra.
62 inline procedural "cic:/CoRN/complex/AbsCC/cc_div_abs.con".
64 inline procedural "cic:/CoRN/complex/AbsCC/cc_div_abs'.con".
66 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_zero.con".
69 Hint Resolve AbsCC_zero: algebra.
72 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_one.con".
74 inline procedural "cic:/CoRN/complex/AbsCC/cc_pow_abs.con".
76 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_pos.con".
78 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_ap_zero.con".
80 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_small_imp_eq.con".
84 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_1_1_2.con" "AbsCC_properties__".
89 Hint Resolve l_1_1_2: algebra.
92 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_square_Re_Im.con".
95 Hint Resolve AbsCC_square_Re_Im: algebra.
100 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_1_2_3_CC.con" "AbsCC_properties__".
105 Hint Resolve l_1_2_3_CC: algebra.
108 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_mult_conj.con".
111 Hint Resolve CC_conj_mult: algebra.
116 inline procedural "cic:/CoRN/complex/AbsCC/l_2_1_2.con".
119 Hint Resolve l_2_1_2: algebra.
124 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_mult_square.con".
126 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_square_ap_zero.con".
128 inline procedural "cic:/CoRN/complex/AbsCC/cc_recip_char.con".
130 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_strext.con".
132 inline procedural "cic:/CoRN/complex/AbsCC/AbsSmallCC.con".
134 inline procedural "cic:/CoRN/complex/AbsCC/Cexis_AFS_CC.con".
136 (* The following lemmas are just auxiliary results *)
140 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_1_2.con" "AbsCC_properties__".
142 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_2_3.con" "AbsCC_properties__".
144 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_3_4.con" "AbsCC_properties__".
153 Hint Resolve AbsCC_wd: algebra_c.
157 Hint Resolve cc_inv_abs cc_mult_abs cc_div_abs cc_div_abs' cc_pow_abs
158 AbsCC_zero AbsCC_one AbsCC_IR AbsCC_mult_conj AbsCC_mult_square
159 cc_recip_char: algebra.
162 (*#* ** The triangle inequality *)
164 inline procedural "cic:/CoRN/complex/AbsCC/triangle.con".
166 inline procedural "cic:/CoRN/complex/AbsCC/triangle_Sum.con".