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 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/arith".
19 include "ext/preamble.ma".
22 \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to
23 (\forall (P: Prop).P))))
25 \lambda (n1: nat).(nat_ind (\lambda (n: nat).(\forall (n2: nat).(or (eq nat
26 n n2) ((eq nat n n2) \to (\forall (P: Prop).P))))) (\lambda (n2:
27 nat).(nat_ind (\lambda (n: nat).(or (eq nat O n) ((eq nat O n) \to (\forall
28 (P: Prop).P)))) (or_introl (eq nat O O) ((eq nat O O) \to (\forall (P:
29 Prop).P)) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (eq nat O n)
30 ((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq
31 nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S
32 n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match
33 ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _)
34 \Rightarrow False])) I (S n) H0) in (False_ind P H1))))))) n2)) (\lambda (n:
35 nat).(\lambda (H: ((\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to
36 (\forall (P: Prop).P)))))).(\lambda (n2: nat).(nat_ind (\lambda (n0: nat).(or
37 (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) (or_intror
38 (eq nat (S n) O) ((eq nat (S n) O) \to (\forall (P: Prop).P)) (\lambda (H0:
39 (eq nat (S n) O)).(\lambda (P: Prop).(let H1 \def (eq_ind nat (S n) (\lambda
40 (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
41 False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) (\lambda
42 (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall
43 (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P:
44 Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P:
45 Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0
46 (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P:
47 Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S
48 n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat
49 (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat
50 (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P:
51 Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
52 (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P:
53 Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return
54 (\lambda (_: nat).nat) with [O \Rightarrow n | (S n) \Rightarrow n])) (S n)
55 (S n0) H2) in (let H4 \def (eq_ind_r nat n0 (\lambda (n0: nat).((eq nat n n0)
56 \to (\forall (P: Prop).P))) H1 n H3) in (let H5 \def (eq_ind_r nat n0
57 (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P:
58 Prop).P)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).
61 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n)
62 (plus p n)) \to (eq nat m p))))
64 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat
65 (plus m n) (plus p n))).(plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda
66 (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0:
67 nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n
68 p)) (plus m n) H) (plus n m) (plus_comm n m)))))).
71 \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
73 \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0:
74 nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_comm m n))).
76 theorem plus_permute_2_in_3:
77 \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x
78 y) z) (plus (plus x z) y))))
80 \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(eq_ind_r nat (plus x
81 (plus y z)) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) (eq_ind_r nat
82 (plus z y) (\lambda (n: nat).(eq nat (plus x n) (plus (plus x z) y))) (eq_ind
83 nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y)))
84 (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_reverse
85 x z y)) (plus y z) (plus_comm y z)) (plus (plus x y) z) (plus_assoc_reverse x
88 theorem plus_permute_2_in_3_assoc:
89 \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n
90 h) k) (plus n (plus k h)))))
92 \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(eq_ind_r nat (plus
93 (plus n k) h) (\lambda (n0: nat).(eq nat n0 (plus n (plus k h)))) (eq_ind_r
94 nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0))
95 (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc n k h))
96 (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
99 \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat
102 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus
103 n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda
104 (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O)
105 H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O)
106 \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq
107 nat (plus (S n) y) O)).(let H1 \def (match H0 in eq return (\lambda (n0:
108 nat).(\lambda (_: (eq ? ? n0)).((eq nat n0 O) \to (land (eq nat (S n) O) (eq
109 nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n)
110 y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e in
111 nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
112 \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y
113 O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
116 \forall (x: nat).(eq nat (minus (S x) (S O)) x)
118 \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal
119 nat x) (minus x O) (minus_n_O x)).
122 \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
124 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq
125 nat n j)) (eq nat n j)))) (\lambda (j: nat).(nat_ind (\lambda (n: nat).(or
126 (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O)
127 (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (not (eq nat O n)) (eq
128 nat O n))).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j))
129 (\lambda (n: nat).(\lambda (H: ((\forall (j: nat).(or (not (eq nat n j)) (eq
130 nat n j))))).(\lambda (j: nat).(nat_ind (\lambda (n0: nat).(or (not (eq nat
131 (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S
132 n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda (n0: nat).(\lambda (_: (or
133 (not (eq nat (S n) n0)) (eq nat (S n) n0))).(or_ind (not (eq nat n n0)) (eq
134 nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda
135 (H1: (not (eq nat n n0))).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S
136 n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not
137 (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H
141 \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j))
142 \to P)) \to ((((eq nat i j) \to P)) \to P))))
144 \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not
145 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def
146 (eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
149 \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S
152 \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P:
153 Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P:
154 Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match
155 H0 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to
156 P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
157 (eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_:
158 nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in
159 (False_ind P H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m)
160 O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat return
161 (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True]))
162 I O H2) in (False_ind ((le (S n) m) \to P) H3)) H1))]) in (H1 (refl_equal nat
163 O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P:
164 Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind
165 (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n))
166 \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S
167 O) (S n))).(let H2 \def (match H0 in le return (\lambda (n: nat).(\lambda (_:
168 (le ? n)).((eq nat n O) \to P))) with [le_n \Rightarrow (\lambda (H2: (eq nat
169 (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e in nat
170 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
171 True])) I O H2) in (False_ind P H3))) | (le_S m H2) \Rightarrow (\lambda (H3:
172 (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m) (\lambda (e: nat).(match e
173 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
174 \Rightarrow True])) I O H3) in (False_ind ((le (S n) m) \to P) H4)) H2))]) in
175 (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P:
176 Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P:
177 Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S
178 n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
181 \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
183 \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def
184 le_Sn_n in (False_ind P (H0 x H))))).
187 \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
189 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n
190 y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall
191 (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(match y in nat return
192 (\lambda (n0: nat).(le (minus (S n) n0) (S n))) with [O \Rightarrow (le_n (S
193 n)) | (S n0) \Rightarrow (le_S (minus n n0) n (H n0))])))) x).
195 theorem le_plus_minus_sym:
196 \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n)
199 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat
200 (plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H)
201 (plus (minus m n) n) (plus_comm (minus m n) n)))).
203 theorem le_minus_minus:
204 \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z)
205 \to (le (minus y x) (minus z x))))))
207 \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z:
208 nat).(\lambda (H0: (le y z)).(plus_le_reg_l x (minus y x) (minus z x)
209 (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat
210 z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z
211 (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
213 theorem le_minus_plus:
214 \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat
215 (minus (plus x y) z) (plus (minus x z) y)))))
217 \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to
218 (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y))))))
219 (\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le return
220 (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) \to (\forall (y:
221 nat).(eq nat (minus (plus x y) O) (plus (minus x O) y)))))) with [le_n
222 \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n:
223 nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))
224 (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O)
225 (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq
226 nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y:
227 nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O
228 m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))])
229 in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x:
230 nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus
231 (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S
232 z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n
233 (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def
234 (match H0 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
235 \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))))) with
236 [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat
237 (S z0) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with
238 [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq
239 nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1)
240 \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m)
241 (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
242 \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S
243 z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3))
244 H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S
245 z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n
246 (S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n
247 (le_S_n z0 n H1) y))))) x)))) z).
250 \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to
251 (le x (minus z y)))))
253 \lambda (x: nat).(\lambda (z: nat).(\lambda (y: nat).(\lambda (H: (le (plus
254 x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z
255 y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x
258 theorem le_trans_plus_r:
259 \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to
262 \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus
263 x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
266 \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n:
267 nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
269 \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def
270 (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x)
271 \to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m
272 n0)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat
273 (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0)))
274 (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S
275 m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x
276 H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat
277 (S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq
278 nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m)
279 m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n:
280 nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2))))
281 x H1 H0))]) in (H0 (refl_equal nat x))))).
283 theorem lt_x_plus_x_Sy:
284 \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
286 \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n:
287 nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x))
288 (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_comm x (S y)))).
290 theorem simpl_lt_plus_r:
291 \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m
294 \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus
295 n p) (plus m p))).(plus_lt_reg_l n m p (let H0 \def (eq_ind nat (plus n p)
296 (\lambda (n: nat).(lt n (plus m p))) H (plus p n) (plus_comm n p)) in (let H1
297 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0 (plus p
298 m) (plus_comm m p)) in H1)))))).
301 \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S
304 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
305 (eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H:
306 (lt y O)).(let H0 \def (match H in le return (\lambda (n: nat).(\lambda (_:
307 (le ? n)).((eq nat n O) \to (eq nat (minus O y) (S (minus O (S y))))))) with
308 [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S
309 y) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
310 \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat
311 (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda
312 (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e:
313 nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False
314 | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat
315 (minus O y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O)))))
316 (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat
317 (minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0:
318 nat).((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))
319 (\lambda (_: (lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S
320 n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0:
321 nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S
322 n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0)
323 n H1) in (H n0 H2))))) y)))) x).
325 theorem lt_plus_minus:
326 \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus
329 \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S
332 theorem lt_plus_minus_r:
333 \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y
336 \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat
337 (plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x
338 y H) (plus (minus y (S x)) x) (plus_comm (minus y (S x)) x)))).
341 \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
343 \lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n:
344 nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal
345 nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
348 \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
350 \lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to
351 (le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def
352 (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
353 \to (le x O)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let
354 H1 \def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat return (\lambda
355 (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0)
356 in (False_ind (le x O) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat
357 (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat
358 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
359 True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0
360 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt
361 x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S
362 n))).(le_S_n x n H0))))) y).
365 \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
367 \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S
368 O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O))
369 (plus_comm x (S O)))))).
372 \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P))
373 \to ((((le d n) \to P)) \to P))))
375 \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n
376 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in
377 (or_ind (le d n) (lt n d) P H0 H H1)))))).
380 \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
381 \to ((((eq nat x y) \to P)) \to ((le x y) \to P)))))
383 \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x
384 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x
385 y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
388 \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
389 \to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P)))))
391 \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x
392 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x)
393 \to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda
394 (H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
397 \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2
398 nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n))))))
400 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).((lt n (S
401 n0)) \to (or (eq nat n O) (ex2 nat (\lambda (m: nat).(eq nat n (S m)))
402 (\lambda (m: nat).(lt m n0))))))) (\lambda (n: nat).(\lambda (_: (lt O (S
403 n))).(or_introl (eq nat O O) (ex2 nat (\lambda (m: nat).(eq nat O (S m)))
404 (\lambda (m: nat).(lt m n))) (refl_equal nat O)))) (\lambda (n: nat).(\lambda
405 (_: ((\forall (n0: nat).((lt n (S n0)) \to (or (eq nat n O) (ex2 nat (\lambda
406 (m: nat).(eq nat n (S m))) (\lambda (m: nat).(lt m n0)))))))).(\lambda (n0:
407 nat).(\lambda (H0: (lt (S n) (S n0))).(or_intror (eq nat (S n) O) (ex2 nat
408 (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0)))
409 (ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt
410 m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
413 \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P:
416 \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt
417 y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
420 \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
422 \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq
423 nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in
424 (lt_irrefl y H1))))).
427 \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n)
428 \to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2))))))
430 \lambda (h2: nat).(\lambda (d2: nat).(\lambda (n: nat).(\lambda (H: (le
431 (plus d2 h2) n)).(\lambda (h1: nat).(eq_ind nat (minus (plus h2 (plus d2 h1))
432 h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2
433 (plus h2 (plus d2 h1)) (le_plus_l h2 (plus d2 h1)) (plus n h1) (eq_ind_r nat
434 (plus (plus h2 d2) h1) (\lambda (n0: nat).(le n0 (plus n h1))) (eq_ind_r nat
435 (plus d2 h2) (\lambda (n0: nat).(le (plus n0 h1) (plus n h1))) (le_S_n (plus
436 (plus d2 h2) h1) (plus n h1) (lt_le_S (plus (plus d2 h2) h1) (S (plus n h1))
437 (le_lt_n_Sm (plus (plus d2 h2) h1) (plus n h1) (plus_le_compat (plus d2 h2) n
438 h1 h1 H (le_n h1))))) (plus h2 d2) (plus_comm h2 d2)) (plus h2 (plus d2 h1))
439 (plus_assoc h2 d2 h1))) (plus d2 h1) (minus_plus h2 (plus d2 h1))))))).
442 \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
444 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to
445 (eq nat (minus n y) O)))) (\lambda (y: nat).(\lambda (_: (le O
446 y)).(refl_equal nat O))) (\lambda (x0: nat).(\lambda (H: ((\forall (y:
447 nat).((le x0 y) \to (eq nat (minus x0 y) O))))).(\lambda (y: nat).(nat_ind
448 (\lambda (n: nat).((le (S x0) n) \to (eq nat (match n with [O \Rightarrow (S
449 x0) | (S l) \Rightarrow (minus x0 l)]) O))) (\lambda (H0: (le (S x0)
450 O)).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le x0
451 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H1: (eq nat O (S
452 x1))).(\lambda (_: (le x0 x1)).(let H3 \def (eq_ind nat O (\lambda (ee:
453 nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
454 | (S _) \Rightarrow False])) I (S x1) H1) in (False_ind (eq nat (S x0) O)
455 H3))))) (le_gen_S x0 O H0))) (\lambda (n: nat).(\lambda (_: (((le (S x0) n)
456 \to (eq nat (match n with [O \Rightarrow (S x0) | (S l) \Rightarrow (minus x0
457 l)]) O)))).(\lambda (H1: (le (S x0) (S n))).(H n (le_S_n x0 n H1))))) y))))
461 \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y)
462 \to ((eq nat (minus x z) (minus y z)) \to (eq nat x y))))))
464 \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).(\forall (y:
465 nat).((le n x) \to ((le n y) \to ((eq nat (minus x n) (minus y n)) \to (eq
466 nat x y))))))) (\lambda (x: nat).(\lambda (y: nat).(\lambda (_: (le O
467 x)).(\lambda (_: (le O y)).(\lambda (H1: (eq nat (minus x O) (minus y
468 O))).(let H2 \def (eq_ind_r nat (minus x O) (\lambda (n: nat).(eq nat n
469 (minus y O))) H1 x (minus_n_O x)) in (let H3 \def (eq_ind_r nat (minus y O)
470 (\lambda (n: nat).(eq nat x n)) H2 y (minus_n_O y)) in H3))))))) (\lambda
471 (z0: nat).(\lambda (IH: ((\forall (x: nat).(\forall (y: nat).((le z0 x) \to
472 ((le z0 y) \to ((eq nat (minus x z0) (minus y z0)) \to (eq nat x
473 y)))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le
474 (S z0) n) \to ((le (S z0) y) \to ((eq nat (minus n (S z0)) (minus y (S z0)))
475 \to (eq nat n y)))))) (\lambda (y: nat).(\lambda (H: (le (S z0) O)).(\lambda
476 (_: (le (S z0) y)).(\lambda (_: (eq nat (minus O (S z0)) (minus y (S
477 z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le
478 z0 n)) (eq nat O y) (\lambda (x0: nat).(\lambda (H2: (eq nat O (S
479 x0))).(\lambda (_: (le z0 x0)).(let H4 \def (eq_ind nat O (\lambda (ee:
480 nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
481 | (S _) \Rightarrow False])) I (S x0) H2) in (False_ind (eq nat O y) H4)))))
482 (le_gen_S z0 O H)))))) (\lambda (x0: nat).(\lambda (_: ((\forall (y:
483 nat).((le (S z0) x0) \to ((le (S z0) y) \to ((eq nat (minus x0 (S z0)) (minus
484 y (S z0))) \to (eq nat x0 y))))))).(\lambda (y: nat).(nat_ind (\lambda (n:
485 nat).((le (S z0) (S x0)) \to ((le (S z0) n) \to ((eq nat (minus (S x0) (S
486 z0)) (minus n (S z0))) \to (eq nat (S x0) n))))) (\lambda (_: (le (S z0) (S
487 x0))).(\lambda (H0: (le (S z0) O)).(\lambda (_: (eq nat (minus (S x0) (S z0))
488 (minus O (S z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda
489 (n: nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H2: (eq
490 nat O (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O (\lambda
491 (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
492 True | (S _) \Rightarrow False])) I (S x1) H2) in (False_ind (eq nat (S x0)
493 O) H4))))) (le_gen_S z0 O H0))))) (\lambda (y0: nat).(\lambda (_: (((le (S
494 z0) (S x0)) \to ((le (S z0) y0) \to ((eq nat (minus (S x0) (S z0)) (minus y0
495 (S z0))) \to (eq nat (S x0) y0)))))).(\lambda (H: (le (S z0) (S
496 x0))).(\lambda (H0: (le (S z0) (S y0))).(\lambda (H1: (eq nat (minus (S x0)
497 (S z0)) (minus (S y0) (S z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0
498 x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z).
501 \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1:
502 nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z
503 x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1)))))))))
505 \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x1: nat).(\forall (x2:
506 nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 n) \to ((le x2 n) \to ((eq
507 nat (plus (minus n x1) y1) (plus (minus n x2) y2)) \to (eq nat (plus x1 y2)
508 (plus x2 y1)))))))))) (\lambda (x1: nat).(\lambda (x2: nat).(\lambda (y1:
509 nat).(\lambda (y2: nat).(\lambda (H: (le x1 O)).(\lambda (H0: (le x2
510 O)).(\lambda (H1: (eq nat y1 y2)).(eq_ind nat y1 (\lambda (n: nat).(eq nat
511 (plus x1 n) (plus x2 y1))) (let H_y \def (le_n_O_eq x2 H0) in (eq_ind nat O
512 (\lambda (n: nat).(eq nat (plus x1 y1) (plus n y1))) (let H_y0 \def
513 (le_n_O_eq x1 H) in (eq_ind nat O (\lambda (n: nat).(eq nat (plus n y1) (plus
514 O y1))) (refl_equal nat (plus O y1)) x1 H_y0)) x2 H_y)) y2 H1))))))))
515 (\lambda (z0: nat).(\lambda (IH: ((\forall (x1: nat).(\forall (x2:
516 nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z0) \to ((le x2 z0) \to
517 ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2)) \to (eq nat (plus
518 x1 y2) (plus x2 y1))))))))))).(\lambda (x1: nat).(nat_ind (\lambda (n:
519 nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le n (S z0))
520 \to ((le x2 (S z0)) \to ((eq nat (plus (minus (S z0) n) y1) (plus (minus (S
521 z0) x2) y2)) \to (eq nat (plus n y2) (plus x2 y1))))))))) (\lambda (x2:
522 nat).(nat_ind (\lambda (n: nat).(\forall (y1: nat).(\forall (y2: nat).((le O
523 (S z0)) \to ((le n (S z0)) \to ((eq nat (plus (minus (S z0) O) y1) (plus
524 (minus (S z0) n) y2)) \to (eq nat (plus O y2) (plus n y1)))))))) (\lambda
525 (y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda (_: (le O
526 (S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (S (plus z0 y2)))).(let H_y
527 \def (IH O O) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n:
528 nat).(\forall (y1: nat).(\forall (y2: nat).((le O z0) \to ((le O z0) \to ((eq
529 nat (plus n y1) (plus n y2)) \to (eq nat y2 y1))))))) H_y z0 (minus_n_O z0))
530 in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (H2 (plus z0 y2) (plus z0 y1) (le_O_n
531 z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1)
532 (sym_equal nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2)
533 H1)))))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall
534 (y2: nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1))
535 (plus (match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)])
536 y2)) \to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2:
537 nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S x3) (S z0))).(\lambda
538 (H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2))).(let H_y \def (IH O
539 x3 (S y1)) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n:
540 nat).(\forall (y2: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S
541 y1)) (plus (minus z0 x3) y2)) \to (eq nat y2 (plus x3 (S y1)))))))) H_y z0
542 (minus_n_O z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda (n:
543 nat).(\forall (y2: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus
544 (minus z0 x3) y2)) \to (eq nat y2 (plus x3 (S y1)))))))) H2 (S (plus z0 y1))
545 (plus_n_Sm z0 y1)) in (let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda
546 (n: nat).(\forall (y2: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus
547 z0 y1)) (plus (minus z0 x3) y2)) \to (eq nat y2 n)))))) H3 (S (plus x3 y1))
548 (plus_n_Sm x3 y1)) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1))))))))))))
549 x2)) (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall (y1:
550 nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat
551 (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2
552 y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(nat_ind (\lambda (n:
553 nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S
554 z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2))
555 \to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda (y1: nat).(\lambda
556 (y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (_: (le O (S
557 z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))).(let
558 H_y \def (IH x2 O y1 (S y2)) in (let H2 \def (eq_ind_r nat (minus z0 O)
559 (\lambda (n: nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2)
560 y1) (plus n (S y2))) \to (eq nat (plus x2 (S y2)) y1))))) H_y z0 (minus_n_O
561 z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda (n: nat).((le x2
562 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (eq nat (plus
563 x2 (S y2)) y1))))) H2 (S (plus z0 y2)) (plus_n_Sm z0 y2)) in (let H4 \def
564 (eq_ind_r nat (plus x2 (S y2)) (\lambda (n: nat).((le x2 z0) \to ((le O z0)
565 \to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1)))))
566 H3 (S (plus x2 y2)) (plus_n_Sm x2 y2)) in (H4 (le_S_n x2 z0 H) (le_O_n z0)
567 H1)))))))))) (\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall
568 (y2: nat).((le (S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus
569 z0 x2) y1) (plus (match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow
570 (minus z0 l)]) y2)) \to (eq nat (S (plus x2 y2)) (plus x4
571 y1))))))))).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S
572 z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0
573 x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4
574 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3))))