helm/software/matita/contribs/procedural/CoRN/complex/AbsCC.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: AbsCC.v,v 1.2 2004/04/23 10:00:54 lcf Exp $ *)
  20
  21 include "complex/CComplex.ma".
  22
  23 (*#* * Absolute value on [CC]
  24 ** Properties of [AbsCC] *)
  25
  26 (* UNEXPORTED
  27 Section AbsCC_properties
  28 *)
  29
  30 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_nonneg.con" as lemma.
  31
  32 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_ap_zero_imp_pos.con" as lemma.
  33
  34 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_wd.con" as lemma.
  35
  36 (* UNEXPORTED
  37 Hint Resolve AbsCC_wd: algebra_c.
  38 *)
  39
  40 inline procedural "cic:/CoRN/complex/AbsCC/cc_inv_abs.con" as lemma.
  41
  42 (* UNEXPORTED
  43 Hint Resolve cc_inv_abs: algebra.
  44 *)
  45
  46 inline procedural "cic:/CoRN/complex/AbsCC/cc_minus_abs.con" as lemma.
  47
  48 inline procedural "cic:/CoRN/complex/AbsCC/cc_mult_abs.con" as lemma.
  49
  50 (* UNEXPORTED
  51 Hint Resolve cc_mult_abs: algebra.
  52 *)
  53
  54 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_minzero.con" as lemma.
  55
  56 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_IR.con" as lemma.
  57
  58 (* UNEXPORTED
  59 Hint Resolve AbsCC_IR: algebra.
  60 *)
  61
  62 inline procedural "cic:/CoRN/complex/AbsCC/cc_div_abs.con" as lemma.
  63
  64 inline procedural "cic:/CoRN/complex/AbsCC/cc_div_abs'.con" as lemma.
  65
  66 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_zero.con" as lemma.
  67
  68 (* UNEXPORTED
  69 Hint Resolve AbsCC_zero: algebra.
  70 *)
  71
  72 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_one.con" as lemma.
  73
  74 inline procedural "cic:/CoRN/complex/AbsCC/cc_pow_abs.con" as lemma.
  75
  76 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_pos.con" as lemma.
  77
  78 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_ap_zero.con" as lemma.
  79
  80 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_small_imp_eq.con" as lemma.
  81
  82 (* begin hide *)
  83
  84 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_1_1_2.con" "AbsCC_properties__" as definition.
  85
  86 (* end hide *)
  87
  88 (* UNEXPORTED
  89 Hint Resolve l_1_1_2: algebra.
  90 *)
  91
  92 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_square_Re_Im.con" as lemma.
  93
  94 (* UNEXPORTED
  95 Hint Resolve AbsCC_square_Re_Im: algebra.
  96 *)
  97
  98 (* begin hide *)
  99
 100 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_1_2_3_CC.con" "AbsCC_properties__" as definition.
 101
 102 (* end hide *)
 103
 104 (* UNEXPORTED
 105 Hint Resolve l_1_2_3_CC: algebra.
 106 *)
 107
 108 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_mult_conj.con" as lemma.
 109
 110 (* UNEXPORTED
 111 Hint Resolve CC_conj_mult: algebra.
 112 *)
 113
 114 (* begin hide *)
 115
 116 inline procedural "cic:/CoRN/complex/AbsCC/l_2_1_2.con" as lemma.
 117
 118 (* UNEXPORTED
 119 Hint Resolve l_2_1_2: algebra.
 120 *)
 121
 122 (* end hide *)
 123
 124 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_mult_square.con" as lemma.
 125
 126 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_square_ap_zero.con" as lemma.
 127
 128 inline procedural "cic:/CoRN/complex/AbsCC/cc_recip_char.con" as lemma.
 129
 130 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_strext.con" as lemma.
 131
 132 inline procedural "cic:/CoRN/complex/AbsCC/AbsSmallCC.con" as definition.
 133
 134 inline procedural "cic:/CoRN/complex/AbsCC/Cexis_AFS_CC.con" as lemma.
 135
 136 (* The following lemmas are just auxiliary results *)
 137
 138 (* begin hide *)
 139
 140 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_1_2.con" "AbsCC_properties__" as definition.
 141
 142 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_2_3.con" "AbsCC_properties__" as definition.
 143
 144 inline procedural "cic:/CoRN/complex/AbsCC/AbsCC_properties/l_4_3_4.con" "AbsCC_properties__" as definition.
 145
 146 (* end hide *)
 147
 148 (* UNEXPORTED
 149 End AbsCC_properties
 150 *)
 151
 152 (* UNEXPORTED
 153 Hint Resolve AbsCC_wd: algebra_c.
 154 *)
 155
 156 (* UNEXPORTED
 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.
 160 *)
 161
 162 (*#* ** The triangle inequality *)
 163
 164 inline procedural "cic:/CoRN/complex/AbsCC/triangle.con" as lemma.
 165
 166 inline procedural "cic:/CoRN/complex/AbsCC/triangle_Sum.con" as lemma.
 167