1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/arith/nat_le.ma".
17 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
20 definition nlt: relation2 nat nat ≝
24 "less (non-negative integers)"
27 (* Basic constructions ******************************************************)
29 lemma nlt_i (m) (n): ↑m ≤ n → m < n.
32 lemma nlt_refl_succ (n): n < ↑n.
36 lemma nlt_zero_succ (m): 𝟎 < ↑m.
37 /2 width=1 by nle_succ_bi/ qed.
39 lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n.
40 /2 width=1 by nle_succ_bi/ qed.
42 (*** le_to_or_lt_eq *)
43 lemma nle_lt_eq_dis (m) (n): m ≤ n → ∨∨ m < n | m = n.
44 #m #n * -n /3 width=1 by nle_succ_bi, or_introl/
48 lemma eq_gt_dis (n): ∨∨ 𝟎 = n | 𝟎 < n.
49 #n elim (nle_lt_eq_dis (𝟎) n ?)
50 /2 width=1 by or_introl, or_intror/
54 lemma nlt_ge_dis (m) (n): ∨∨ m < n | n ≤ m.
55 #m #n elim (nle_ge_dis m n) /2 width=1 by or_intror/
56 #H elim (nle_lt_eq_dis … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
60 lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
61 #m #n elim (nlt_ge_dis m n) [ // ]
65 (*** lt_to_le_to_lt *)
66 lemma nlt_le_trans (o) (m) (n): m < o → o ≤ n → m < n.
67 /2 width=3 by nle_trans/ qed-.
69 (*** le_to_lt_to_lt *)
70 lemma le_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
71 /3 width=3 by nle_succ_bi, nle_trans/ qed-.
73 (* Basic inversions *********************************************************)
75 lemma nlt_inv_succ_bi (m) (n): ↑m < ↑n → m < n.
76 /2 width=1 by nle_inv_succ_bi/ qed-.
79 lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
80 /3 width=4 by nle_inv_succ_sn_refl, nlt_le_trans/ qed-.
83 lemma nlt_inv_refl (m): m < m → ⊥.
84 /2 width=4 by nlt_ge_false/ qed-.
86 lemma nlt_inv_zero_dx (m): m < 𝟎 → ⊥.
87 /2 width=4 by nlt_ge_false/ qed-.
89 (* Basic destructions *******************************************************)
92 lemma nlt_des_le (m) (n): m < n → m ≤ n.
93 /2 width=3 by nle_trans/ qed-.
96 lemma nlt_des_lt_O_sn (m) (n): m < n → 𝟎 < n.
97 /3 width=3 by le_nlt_trans/ qed-.
99 (* Main constructions *******************************************************)
101 (*** transitive_lt *)
102 theorem nlt_trans: Transitive … nlt.
103 /3 width=3 by nlt_des_le, nlt_le_trans/ qed-.
105 (* Advanced eliminations ****************************************************)
107 lemma nat_ind_lt_le (Q:predicate …):
108 (∀n. (∀m. m < n → Q m) → Q n) → ∀n,m. m ≤ n → Q m.
109 #Q #H1 #n @(nat_ind_succ … n) -n
110 [ #m #H <(nle_inv_zero_dx … H) -m
111 @H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
112 | /5 width=3 by nlt_le_trans, nle_inv_succ_bi/
117 lemma nat_ind_lt (Q:predicate …):
118 (∀n. (∀m. m < n → Q m) → Q n) → ∀n. Q n.
119 /4 width=2 by nat_ind_lt_le/ qed-.
122 lemma nlt_ind_alt (Q: relation2 nat nat):
124 (∀m,n. m < n → Q m n → Q (↑m) (↑n)) →
126 #Q #IH1 #IH2 #m #n @(nat_ind_succ_2 … n m) -m -n //
128 elim (nlt_inv_zero_dx … H)
129 | /4 width=1 by nlt_inv_succ_bi/