]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/nlibrary/nat/order.ma
- main proposition on lsx finally proved!
[helm.git] / matita / 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 → ext_powerclass NAT.
46  #n; napply mk_ext_powerclass
47   [ napply {m | m < n}
48   | #x; #x'; #H; nrewrite < H; napply mk_iff; #K; nassumption (* refl non va *) ]
49 nqed.