matita/contribs/CoRN-Decl/algebra/Expon.ma

   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 set "baseuri" "cic:/matita/CoRN-Decl/algebra/Expon".
  18
  19 include "CoRN_notation.ma".
  20
  21 (* $Id: Expon.v,v 1.5 2004/04/23 10:00:54 lcf Exp $ *)
  22
  23 (*#* printing [^^] %\ensuremath{\hat{\ }}% #^# *)
  24
  25 include "algebra/COrdCauchy.ma".
  26
  27 include "tactics/Transparent_algebra.ma".
  28
  29 (*#* *Exponentiation
  30 **More properties about [nexp]
  31 %\begin{convention}% Let [R] be an ordered field.
  32 %\end{convention}%
  33 *)
  34
  35 (* UNEXPORTED
  36 Section More_Nexp.
  37 *)
  38
  39 inline "cic:/CoRN/algebra/Expon/R.var".
  40
  41 inline "cic:/CoRN/algebra/Expon/nexp_resp_ap_zero.con".
  42
  43 (* UNEXPORTED
  44 Hint Resolve nexp_resp_ap_zero: algebra.
  45 *)
  46
  47 inline "cic:/CoRN/algebra/Expon/nexp_distr_div.con".
  48
  49 inline "cic:/CoRN/algebra/Expon/nexp_distr_div'.con".
  50
  51 inline "cic:/CoRN/algebra/Expon/small_nexp_resp_lt.con".
  52
  53 inline "cic:/CoRN/algebra/Expon/great_nexp_resp_lt.con".
  54
  55 inline "cic:/CoRN/algebra/Expon/small_nexp_resp_le.con".
  56
  57 inline "cic:/CoRN/algebra/Expon/great_nexp_resp_le.con".
  58
  59 inline "cic:/CoRN/algebra/Expon/nexp_resp_leEq.con".
  60
  61 inline "cic:/CoRN/algebra/Expon/nexp_resp_leEq_one.con".
  62
  63 inline "cic:/CoRN/algebra/Expon/nexp_resp_leEq_neg_even.con".
  64
  65 inline "cic:/CoRN/algebra/Expon/nexp_resp_leEq_neg_odd.con".
  66
  67 inline "cic:/CoRN/algebra/Expon/nexp_distr_recip.con".
  68
  69 (* UNEXPORTED
  70 Hint Resolve nexp_distr_recip: algebra.
  71 *)
  72
  73 inline "cic:/CoRN/algebra/Expon/nexp_even_nonneg.con".
  74
  75 inline "cic:/CoRN/algebra/Expon/nexp_resp_le'.con".
  76
  77 inline "cic:/CoRN/algebra/Expon/nexp_resp_le.con".
  78
  79 inline "cic:/CoRN/algebra/Expon/bin_less_un.con".
  80
  81 (* UNEXPORTED
  82 End More_Nexp.
  83 *)
  84
  85 (* UNEXPORTED
  86 Hint Resolve nexp_distr_div nexp_distr_recip: algebra.
  87 *)
  88
  89 (* UNEXPORTED
  90 Implicit Arguments nexp_resp_ap_zero [R x].
  91 *)
  92
  93 (*#* **Definition of [zexp]: integer exponentiation
  94 %\begin{convention}% Let [R] be an ordered field.
  95 %\end{convention}%
  96 *)
  97
  98 (* UNEXPORTED
  99 Section Zexp_def.
 100 *)
 101
 102 inline "cic:/CoRN/algebra/Expon/R.var".
 103
 104 (*#*
 105 It would be nicer to define [zexp] using [caseZdiff], but we already
 106 have most properties now.
 107 *)
 108
 109 inline "cic:/CoRN/algebra/Expon/zexp.con".
 110
 111 (* UNEXPORTED
 112 End Zexp_def.
 113 *)
 114
 115 (* UNEXPORTED
 116 Implicit Arguments zexp [R].
 117 *)
 118
 119 (*#* **Properties of [zexp]
 120 %\begin{convention}% Let [R] be an ordered field.
 121 %\end{convention}%
 122 *)
 123
 124 (* UNEXPORTED
 125 Section Zexp_properties.
 126 *)
 127
 128 inline "cic:/CoRN/algebra/Expon/R.var".
 129
 130 inline "cic:/CoRN/algebra/Expon/zexp_zero.con".
 131
 132 (* UNEXPORTED
 133 Hint Resolve zexp_zero: algebra.
 134 *)
 135
 136 inline "cic:/CoRN/algebra/Expon/zexp_nexp.con".
 137
 138 (* UNEXPORTED
 139 Hint Resolve zexp_nexp: algebra.
 140 *)
 141
 142 inline "cic:/CoRN/algebra/Expon/zexp_inv_nexp.con".
 143
 144 (* UNEXPORTED
 145 Hint Resolve zexp_inv_nexp: algebra.
 146 *)
 147
 148 inline "cic:/CoRN/algebra/Expon/zexp_inv_nexp'.con".
 149
 150 (* UNEXPORTED
 151 Hint Resolve zexp_inv_nexp': algebra.
 152 *)
 153
 154 inline "cic:/CoRN/algebra/Expon/zexp_strext.con".
 155
 156 inline "cic:/CoRN/algebra/Expon/zexp_wd.con".
 157
 158 (* UNEXPORTED
 159 Hint Resolve zexp_wd: algebra_c.
 160 *)
 161
 162 inline "cic:/CoRN/algebra/Expon/zexp_plus1.con".
 163
 164 (* UNEXPORTED
 165 Hint Resolve zexp_plus1: algebra.
 166 *)
 167
 168 inline "cic:/CoRN/algebra/Expon/zexp_resp_ap_zero.con".
 169
 170 (* UNEXPORTED
 171 Hint Resolve zexp_resp_ap_zero: algebra.
 172 *)
 173
 174 inline "cic:/CoRN/algebra/Expon/zexp_inv.con".
 175
 176 (* UNEXPORTED
 177 Hint Resolve zexp_inv: algebra.
 178 *)
 179
 180 inline "cic:/CoRN/algebra/Expon/zexp_inv1.con".
 181
 182 (* UNEXPORTED
 183 Hint Resolve zexp_inv1: algebra.
 184 *)
 185
 186 inline "cic:/CoRN/algebra/Expon/zexp_plus.con".
 187
 188 (* UNEXPORTED
 189 Hint Resolve zexp_plus: algebra.
 190 *)
 191
 192 inline "cic:/CoRN/algebra/Expon/zexp_minus.con".
 193
 194 (* UNEXPORTED
 195 Hint Resolve zexp_minus: algebra.
 196 *)
 197
 198 inline "cic:/CoRN/algebra/Expon/one_zexp.con".
 199
 200 (* UNEXPORTED
 201 Hint Resolve one_zexp: algebra.
 202 *)
 203
 204 inline "cic:/CoRN/algebra/Expon/mult_zexp.con".
 205
 206 (* UNEXPORTED
 207 Hint Resolve mult_zexp: algebra.
 208 *)
 209
 210 inline "cic:/CoRN/algebra/Expon/zexp_mult.con".
 211
 212 (* UNEXPORTED
 213 Hint Resolve zexp_mult: algebra.
 214 *)
 215
 216 inline "cic:/CoRN/algebra/Expon/zexp_two.con".
 217
 218 (* UNEXPORTED
 219 Hint Resolve zexp_two: algebra.
 220 *)
 221
 222 inline "cic:/CoRN/algebra/Expon/inv_zexp_even.con".
 223
 224 (* UNEXPORTED
 225 Hint Resolve inv_zexp_even: algebra.
 226 *)
 227
 228 inline "cic:/CoRN/algebra/Expon/inv_zexp_two.con".
 229
 230 (* UNEXPORTED
 231 Hint Resolve inv_zexp_two: algebra.
 232 *)
 233
 234 inline "cic:/CoRN/algebra/Expon/inv_zexp_odd.con".
 235
 236 inline "cic:/CoRN/algebra/Expon/zexp_one.con".
 237
 238 (* UNEXPORTED
 239 Hint Resolve zexp_one: algebra.
 240 *)
 241
 242 inline "cic:/CoRN/algebra/Expon/zexp_funny.con".
 243
 244 (* UNEXPORTED
 245 Hint Resolve zexp_funny: algebra.
 246 *)
 247
 248 inline "cic:/CoRN/algebra/Expon/zexp_funny'.con".
 249
 250 (* UNEXPORTED
 251 Hint Resolve zexp_funny': algebra.
 252 *)
 253
 254 inline "cic:/CoRN/algebra/Expon/zexp_pos.con".
 255
 256 (* UNEXPORTED
 257 End Zexp_properties.
 258 *)
 259
 260 (* UNEXPORTED
 261 Hint Resolve nexp_resp_ap_zero zexp_zero zexp_nexp zexp_inv_nexp
 262   zexp_inv_nexp' zexp_plus1 zexp_resp_ap_zero zexp_inv zexp_inv1 zexp_plus
 263   zexp_minus one_zexp mult_zexp zexp_mult zexp_two inv_zexp_even inv_zexp_two
 264   zexp_one zexp_funny zexp_funny': algebra.
 265 *)
 266
 267 (* UNEXPORTED
 268 Hint Resolve zexp_wd: algebra_c.
 269 *)
 270
 271 (* UNEXPORTED
 272 Section Root_Unique.
 273 *)
 274
 275 inline "cic:/CoRN/algebra/Expon/R.var".
 276
 277 inline "cic:/CoRN/algebra/Expon/root_unique.con".
 278
 279 inline "cic:/CoRN/algebra/Expon/root_one.con".
 280
 281 (* UNEXPORTED
 282 End Root_Unique.
 283 *)
 284