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" as lemma.
32 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_ap_zero_imp_pos.con" as lemma.
34 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_wd.con" as lemma.
37 Hint Resolve AbsCC_wd: algebra_c.
40 inline procedural "cic:/CoRN/complex/AbsCC/cc_inv_abs.con" as lemma.
43 Hint Resolve cc_inv_abs: algebra.
46 inline procedural "cic:/CoRN/complex/AbsCC/cc_minus_abs.con" as lemma.
48 inline procedural "cic:/CoRN/complex/AbsCC/cc_mult_abs.con" as lemma.
51 Hint Resolve cc_mult_abs: algebra.
54 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_minzero.con" as lemma.
56 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_IR.con" as lemma.
59 Hint Resolve AbsCC_IR: algebra.
62 inline procedural "cic:/CoRN/complex/AbsCC/cc_div_abs.con" as lemma.
64 inline procedural "cic:/CoRN/complex/AbsCC/cc_div_abs'.con" as lemma.
66 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_zero.con" as lemma.
69 Hint Resolve AbsCC_zero: algebra.
72 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_one.con" as lemma.
74 inline procedural "cic:/CoRN/complex/AbsCC/cc_pow_abs.con" as lemma.
76 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_pos.con" as lemma.
78 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_ap_zero.con" as lemma.
80 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_small_imp_eq.con" as lemma.
84 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_1_1_2.con" "AbsCC_properties__" as definition.
89 Hint Resolve l_1_1_2: algebra.
92 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_square_Re_Im.con" as lemma.
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__" as definition.
105 Hint Resolve l_1_2_3_CC: algebra.
108 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_mult_conj.con" as lemma.
111 Hint Resolve CC_conj_mult: algebra.
116 inline procedural "cic:/CoRN/complex/AbsCC/l_2_1_2.con" as lemma.
119 Hint Resolve l_2_1_2: algebra.
124 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_mult_square.con" as lemma.
126 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_square_ap_zero.con" as lemma.
128 inline procedural "cic:/CoRN/complex/AbsCC/cc_recip_char.con" as lemma.
130 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_strext.con" as lemma.
132 inline procedural "cic:/CoRN/complex/AbsCC/AbsSmallCC.con" as definition.
134 inline procedural "cic:/CoRN/complex/AbsCC/Cexis_AFS_CC.con" as lemma.
136 (* The following lemmas are just auxiliary results *)
140 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_1_2.con" "AbsCC_properties__" as definition.
142 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_2_3.con" "AbsCC_properties__" as definition.
144 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_3_4.con" "AbsCC_properties__" as definition.
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" as lemma.
166 inline procedural "cic:/CoRN/complex/AbsCC/triangle_Sum.con" as lemma.