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.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 alias id "R" = "cic:/CoRN/algebra/Expon/More_Nexp/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 alias id "R" = "cic:/CoRN/algebra/Expon/Zexp_def/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 (* NOTATION
 120 Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
 121 *)
 122
 123 (*#* **Properties of [zexp]
 124 %\begin{convention}% Let [R] be an ordered field.
 125 %\end{convention}%
 126 *)
 127
 128 (* UNEXPORTED
 129 Section Zexp_properties
 130 *)
 131
 132 alias id "R" = "cic:/CoRN/algebra/Expon/Zexp_properties/R.var".
 133
 134 inline "cic:/CoRN/algebra/Expon/zexp_zero.con".
 135
 136 (* UNEXPORTED
 137 Hint Resolve zexp_zero: algebra.
 138 *)
 139
 140 inline "cic:/CoRN/algebra/Expon/zexp_nexp.con".
 141
 142 (* UNEXPORTED
 143 Hint Resolve zexp_nexp: algebra.
 144 *)
 145
 146 inline "cic:/CoRN/algebra/Expon/zexp_inv_nexp.con".
 147
 148 (* UNEXPORTED
 149 Hint Resolve zexp_inv_nexp: algebra.
 150 *)
 151
 152 inline "cic:/CoRN/algebra/Expon/zexp_inv_nexp'.con".
 153
 154 (* UNEXPORTED
 155 Hint Resolve zexp_inv_nexp': algebra.
 156 *)
 157
 158 inline "cic:/CoRN/algebra/Expon/zexp_strext.con".
 159
 160 inline "cic:/CoRN/algebra/Expon/zexp_wd.con".
 161
 162 (* UNEXPORTED
 163 Hint Resolve zexp_wd: algebra_c.
 164 *)
 165
 166 inline "cic:/CoRN/algebra/Expon/zexp_plus1.con".
 167
 168 (* UNEXPORTED
 169 Hint Resolve zexp_plus1: algebra.
 170 *)
 171
 172 inline "cic:/CoRN/algebra/Expon/zexp_resp_ap_zero.con".
 173
 174 (* UNEXPORTED
 175 Hint Resolve zexp_resp_ap_zero: algebra.
 176 *)
 177
 178 inline "cic:/CoRN/algebra/Expon/zexp_inv.con".
 179
 180 (* UNEXPORTED
 181 Hint Resolve zexp_inv: algebra.
 182 *)
 183
 184 inline "cic:/CoRN/algebra/Expon/zexp_inv1.con".
 185
 186 (* UNEXPORTED
 187 Hint Resolve zexp_inv1: algebra.
 188 *)
 189
 190 inline "cic:/CoRN/algebra/Expon/zexp_plus.con".
 191
 192 (* UNEXPORTED
 193 Hint Resolve zexp_plus: algebra.
 194 *)
 195
 196 inline "cic:/CoRN/algebra/Expon/zexp_minus.con".
 197
 198 (* UNEXPORTED
 199 Hint Resolve zexp_minus: algebra.
 200 *)
 201
 202 inline "cic:/CoRN/algebra/Expon/one_zexp.con".
 203
 204 (* UNEXPORTED
 205 Hint Resolve one_zexp: algebra.
 206 *)
 207
 208 inline "cic:/CoRN/algebra/Expon/mult_zexp.con".
 209
 210 (* UNEXPORTED
 211 Hint Resolve mult_zexp: algebra.
 212 *)
 213
 214 inline "cic:/CoRN/algebra/Expon/zexp_mult.con".
 215
 216 (* UNEXPORTED
 217 Hint Resolve zexp_mult: algebra.
 218 *)
 219
 220 inline "cic:/CoRN/algebra/Expon/zexp_two.con".
 221
 222 (* UNEXPORTED
 223 Hint Resolve zexp_two: algebra.
 224 *)
 225
 226 inline "cic:/CoRN/algebra/Expon/inv_zexp_even.con".
 227
 228 (* UNEXPORTED
 229 Hint Resolve inv_zexp_even: algebra.
 230 *)
 231
 232 inline "cic:/CoRN/algebra/Expon/inv_zexp_two.con".
 233
 234 (* UNEXPORTED
 235 Hint Resolve inv_zexp_two: algebra.
 236 *)
 237
 238 inline "cic:/CoRN/algebra/Expon/inv_zexp_odd.con".
 239
 240 inline "cic:/CoRN/algebra/Expon/zexp_one.con".
 241
 242 (* UNEXPORTED
 243 Hint Resolve zexp_one: algebra.
 244 *)
 245
 246 inline "cic:/CoRN/algebra/Expon/zexp_funny.con".
 247
 248 (* UNEXPORTED
 249 Hint Resolve zexp_funny: algebra.
 250 *)
 251
 252 inline "cic:/CoRN/algebra/Expon/zexp_funny'.con".
 253
 254 (* UNEXPORTED
 255 Hint Resolve zexp_funny': algebra.
 256 *)
 257
 258 inline "cic:/CoRN/algebra/Expon/zexp_pos.con".
 259
 260 (* UNEXPORTED
 261 End Zexp_properties
 262 *)
 263
 264 (* UNEXPORTED
 265 Hint Resolve nexp_resp_ap_zero zexp_zero zexp_nexp zexp_inv_nexp
 266   zexp_inv_nexp' zexp_plus1 zexp_resp_ap_zero zexp_inv zexp_inv1 zexp_plus
 267   zexp_minus one_zexp mult_zexp zexp_mult zexp_two inv_zexp_even inv_zexp_two
 268   zexp_one zexp_funny zexp_funny': algebra.
 269 *)
 270
 271 (* UNEXPORTED
 272 Hint Resolve zexp_wd: algebra_c.
 273 *)
 274
 275 (* UNEXPORTED
 276 Section Root_Unique
 277 *)
 278
 279 alias id "R" = "cic:/CoRN/algebra/Expon/Root_Unique/R.var".
 280
 281 inline "cic:/CoRN/algebra/Expon/root_unique.con".
 282
 283 inline "cic:/CoRN/algebra/Expon/root_one.con".
 284
 285 (* UNEXPORTED
 286 End Root_Unique
 287 *)
 288