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