helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.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 "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Zorder.v,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
  34
  35 (*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *)
  36
  37 include "NArith/BinPos.ma".
  38
  39 include "ZArith/BinInt.ma".
  40
  41 include "Arith/Arith.ma".
  42
  43 include "Logic/Decidable.ma".
  44
  45 include "ZArith/Zcompare.ma".
  46
  47 (* UNEXPORTED
  48 Open Local Scope Z_scope.
  49 *)
  50
  51 (* UNEXPORTED
  52 Implicit Types x y z : Z.
  53 *)
  54
  55 (*#*********************************************************************)
  56
  57 (*#* Properties of the order relations on binary integers *)
  58
  59 (*#* Trichotomy *)
  60
  61 inline procedural "cic:/Coq/ZArith/Zorder/Ztrichotomy_inf.con" as theorem.
  62
  63 inline procedural "cic:/Coq/ZArith/Zorder/Ztrichotomy.con" as theorem.
  64
  65 (*#*********************************************************************)
  66
  67 (*#* Decidability of equality and order on Z *)
  68
  69 inline procedural "cic:/Coq/ZArith/Zorder/dec_eq.con" as theorem.
  70
  71 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zne.con" as theorem.
  72
  73 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zle.con" as theorem.
  74
  75 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zgt.con" as theorem.
  76
  77 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zge.con" as theorem.
  78
  79 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zlt.con" as theorem.
  80
  81 inline procedural "cic:/Coq/ZArith/Zorder/not_Zeq.con" as theorem.
  82
  83 (*#* Relating strict and large orders *)
  84
  85 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_lt.con" as lemma.
  86
  87 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_gt.con" as lemma.
  88
  89 inline procedural "cic:/Coq/ZArith/Zorder/Zge_le.con" as lemma.
  90
  91 inline procedural "cic:/Coq/ZArith/Zorder/Zle_ge.con" as lemma.
  92
  93 inline procedural "cic:/Coq/ZArith/Zorder/Zle_not_gt.con" as lemma.
  94
  95 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_not_le.con" as lemma.
  96
  97 inline procedural "cic:/Coq/ZArith/Zorder/Zle_not_lt.con" as lemma.
  98
  99 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_not_le.con" as lemma.
 100
 101 inline procedural "cic:/Coq/ZArith/Zorder/Znot_ge_lt.con" as lemma.
 102
 103 inline procedural "cic:/Coq/ZArith/Zorder/Znot_lt_ge.con" as lemma.
 104
 105 inline procedural "cic:/Coq/ZArith/Zorder/Znot_gt_le.con" as lemma.
 106
 107 inline procedural "cic:/Coq/ZArith/Zorder/Znot_le_gt.con" as lemma.
 108
 109 inline procedural "cic:/Coq/ZArith/Zorder/Zge_iff_le.con" as lemma.
 110
 111 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_iff_lt.con" as lemma.
 112
 113 (*#* Reflexivity *)
 114
 115 inline procedural "cic:/Coq/ZArith/Zorder/Zle_refl.con" as lemma.
 116
 117 inline procedural "cic:/Coq/ZArith/Zorder/Zeq_le.con" as lemma.
 118
 119 (* UNEXPORTED
 120 Hint Resolve Zle_refl: zarith.
 121 *)
 122
 123 (*#* Antisymmetry *)
 124
 125 inline procedural "cic:/Coq/ZArith/Zorder/Zle_antisym.con" as lemma.
 126
 127 (*#* Asymmetry *)
 128
 129 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_asym.con" as lemma.
 130
 131 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_asym.con" as lemma.
 132
 133 (*#* Irreflexivity *)
 134
 135 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_irrefl.con" as lemma.
 136
 137 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_irrefl.con" as lemma.
 138
 139 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_not_eq.con" as lemma.
 140
 141 (*#* Large = strict or equal *)
 142
 143 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_le_weak.con" as lemma.
 144
 145 inline procedural "cic:/Coq/ZArith/Zorder/Zle_lt_or_eq.con" as lemma.
 146
 147 (*#* Dichotomy *)
 148
 149 inline procedural "cic:/Coq/ZArith/Zorder/Zle_or_lt.con" as lemma.
 150
 151 (*#* Transitivity of strict orders *)
 152
 153 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_trans.con" as lemma.
 154
 155 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_trans.con" as lemma.
 156
 157 (*#* Mixed transitivity *)
 158
 159 inline procedural "cic:/Coq/ZArith/Zorder/Zle_gt_trans.con" as lemma.
 160
 161 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_le_trans.con" as lemma.
 162
 163 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_le_trans.con" as lemma.
 164
 165 inline procedural "cic:/Coq/ZArith/Zorder/Zle_lt_trans.con" as lemma.
 166
 167 (*#* Transitivity of large orders *)
 168
 169 inline procedural "cic:/Coq/ZArith/Zorder/Zle_trans.con" as lemma.
 170
 171 inline procedural "cic:/Coq/ZArith/Zorder/Zge_trans.con" as lemma.
 172
 173 (* UNEXPORTED
 174 Hint Resolve Zle_trans: zarith.
 175 *)
 176
 177 (*#* Compatibility of successor wrt to order *)
 178
 179 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_le_compat.con" as lemma.
 180
 181 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_gt_compat.con" as lemma.
 182
 183 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_lt_compat.con" as lemma.
 184
 185 (* UNEXPORTED
 186 Hint Resolve Zsucc_le_compat: zarith.
 187 *)
 188
 189 (*#* Simplification of successor wrt to order *)
 190
 191 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_gt_reg.con" as lemma.
 192
 193 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_le_reg.con" as lemma.
 194
 195 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_lt_reg.con" as lemma.
 196
 197 (*#* Compatibility of addition wrt to order *)
 198
 199 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_compat_l.con" as lemma.
 200
 201 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_compat_r.con" as lemma.
 202
 203 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_compat_l.con" as lemma.
 204
 205 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_compat_r.con" as lemma.
 206
 207 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con" as lemma.
 208
 209 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_compat_r.con" as lemma.
 210
 211 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_le_compat.con" as lemma.
 212
 213 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con" as lemma.
 214
 215 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_compat.con" as lemma.
 216
 217 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con" as lemma.
 218
 219 (*#* Compatibility of addition wrt to being positive *)
 220
 221 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con" as lemma.
 222
 223 (*#* Simplification of addition wrt to order *)
 224
 225 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_reg_l.con" as lemma.
 226
 227 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_reg_r.con" as lemma.
 228
 229 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_reg_l.con" as lemma.
 230
 231 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_reg_r.con" as lemma.
 232
 233 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_reg_l.con" as lemma.
 234
 235 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_reg_r.con" as lemma.
 236
 237 (*#* Special base instances of order *)
 238
 239 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ.con" as lemma.
 240
 241 inline procedural "cic:/Coq/ZArith/Zorder/Znot_le_succ.con" as lemma.
 242
 243 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ.con" as lemma.
 244
 245 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_pred.con" as lemma.
 246
 247 (*#* Relating strict and large order using successor or predecessor *)
 248
 249 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_le_succ.con" as lemma.
 250
 251 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_gt_succ.con" as lemma.
 252
 253 inline procedural "cic:/Coq/ZArith/Zorder/Zle_lt_succ.con" as lemma.
 254
 255 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_le_succ.con" as lemma.
 256
 257 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ_le.con" as lemma.
 258
 259 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ_le.con" as lemma.
 260
 261 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ_gt.con" as lemma.
 262
 263 (*#* Weakening order *)
 264
 265 inline procedural "cic:/Coq/ZArith/Zorder/Zle_succ.con" as lemma.
 266
 267 (* UNEXPORTED
 268 Hint Resolve Zle_succ: zarith.
 269 *)
 270
 271 inline procedural "cic:/Coq/ZArith/Zorder/Zle_pred.con" as lemma.
 272
 273 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_lt_succ.con" as lemma.
 274
 275 inline procedural "cic:/Coq/ZArith/Zorder/Zle_le_succ.con" as lemma.
 276
 277 inline procedural "cic:/Coq/ZArith/Zorder/Zle_succ_le.con" as lemma.
 278
 279 (* UNEXPORTED
 280 Hint Resolve Zle_le_succ: zarith.
 281 *)
 282
 283 (*#* Relating order wrt successor and order wrt predecessor *)
 284
 285 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ_pred.con" as lemma.
 286
 287 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ_pred.con" as lemma.
 288
 289 (*#* Relating strict order and large order on positive *)
 290
 291 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_0_le_0_pred.con" as lemma.
 292
 293 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_0_le_0_pred.con" as lemma.
 294
 295 (*#* Special cases of ordered integers *)
 296
 297 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_0_1.con" as lemma.
 298
 299 inline procedural "cic:/Coq/ZArith/Zorder/Zle_0_1.con" as lemma.
 300
 301 inline procedural "cic:/Coq/ZArith/Zorder/Zle_neg_pos.con" as lemma.
 302
 303 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_pos_0.con" as lemma.
 304
 305 (* weaker but useful (in [Zpower] for instance) *)
 306
 307 inline procedural "cic:/Coq/ZArith/Zorder/Zle_0_pos.con" as lemma.
 308
 309 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_neg_0.con" as lemma.
 310
 311 inline procedural "cic:/Coq/ZArith/Zorder/Zle_0_nat.con" as lemma.
 312
 313 (* UNEXPORTED
 314 Hint Immediate Zeq_le: zarith.
 315 *)
 316
 317 (*#* Transitivity using successor *)
 318
 319 inline procedural "cic:/Coq/ZArith/Zorder/Zge_trans_succ.con" as lemma.
 320
 321 (*#* Derived lemma *)
 322
 323 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ_gt_or_eq.con" as lemma.
 324
 325 (*#* Compatibility of multiplication by a positive wrt to order *)
 326
 327 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_compat_r.con" as lemma.
 328
 329 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_compat_l.con" as lemma.
 330
 331 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_compat_r.con" as lemma.
 332
 333 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_compat_r.con" as lemma.
 334
 335 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_compat_r.con" as lemma.
 336
 337 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_le_compat_r.con" as lemma.
 338
 339 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_0_le_compat_r.con" as lemma.
 340
 341 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_compat_l.con" as lemma.
 342
 343 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con" as lemma.
 344
 345 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_compat_l.con" as lemma.
 346
 347 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_compat_r.con" as lemma.
 348
 349 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_compat_l.con" as lemma.
 350
 351 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_compat.con" as lemma.
 352
 353 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_compat.con" as lemma.
 354
 355 (*#* Simplification of multiplication by a positive wrt to being positive *)
 356
 357 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_reg_r.con" as lemma.
 358
 359 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_reg_r.con" as lemma.
 360
 361 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_reg_r.con" as lemma.
 362
 363 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_0_le_reg_r.con" as lemma.
 364
 365 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_reg_r.con" as lemma.
 366
 367 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_reg_r.con" as lemma.
 368
 369 (*#* Compatibility of multiplication by a positive wrt to being positive *)
 370
 371 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con" as lemma.
 372
 373 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_compat.con" as lemma.
 374
 375 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con" as lemma.
 376
 377 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_le_0_compat.con" as lemma.
 378
 379 (*#* Simplification of multiplication by a positive wrt to being positive *)
 380
 381 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_0_reg_r.con" as lemma.
 382
 383 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_0_reg_r.con" as lemma.
 384
 385 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_0_reg_r.con" as lemma.
 386
 387 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_reg_l.con" as lemma.
 388
 389 (*#* Simplification of square wrt order *)
 390
 391 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_square_simpl.con" as lemma.
 392
 393 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_square_simpl.con" as lemma.
 394
 395 (*#* Equivalence between inequalities *)
 396
 397 inline procedural "cic:/Coq/ZArith/Zorder/Zle_plus_swap.con" as lemma.
 398
 399 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_plus_swap.con" as lemma.
 400
 401 inline procedural "cic:/Coq/ZArith/Zorder/Zeq_plus_swap.con" as lemma.
 402
 403 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_minus_simpl_swap.con" as lemma.
 404
 405 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_O_minus_lt.con" as lemma.
 406