helm/software/matita/nlibrary/nat/order.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 include "nat/nat.ma".
  16 include "sets/sets.ma".
  17
  18 ninductive le (n: nat) : nat → CProp[0] ≝
  19    le_n: le n n
  20  | le_S: ∀m. le n m → le n (S m).
  21
  22 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
  23 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
  24
  25 ndefinition lt ≝ λn,m. S n ≤ m.
  26
  27 interpretation "natural 'less than'" 'lt x y = (lt x y).
  28 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
  29
  30 nlemma le_O_n: ∀n. le O n.
  31  #n; nelim n [ napply le_n | #n'; #H; napply le_S; nassumption ]
  32 nqed.
  33
  34 (* needs decompose *)
  35 naxiom le_S_S: ∀n,m. le n m → le (S n) (S m).
  36 naxiom le_S_S_to_le: ∀n,m. le (S n) (S m) → le n m.
  37 naxiom lt_Sn_m: ∀n,m. lt (S n) m → lt n m.
  38 naxiom lt_to_le: ∀n,m. lt n m → le n m.
  39 naxiom lt_le_trans: ∀n,m,p. lt n m → le m p → lt n p.
  40
  41 nlemma lt_O_Sn: ∀n. lt O (S n).
  42  #n; napply le_S_S; napply le_O_n.
  43 nqed.
  44
  45 ndefinition Nat_: nat → qpowerclass NAT.
  46  #n; napply mk_qpowerclass
  47   [ napply {m | m < n}
  48   | #x; #x'; #H; nrewrite < H; napply mk_iff; #K; nassumption (* refl non va *) ]
  49 nqed.