]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma
- ground_2: some additions
[helm.git] / matita / matita / contribs / lambdadelta / ground_1 / ext / arith.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 (* This file was automatically generated: do not edit *********************)
16
17 include "ground_1/preamble.ma".
18
19 lemma nat_dec:
20  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 
21 (\forall (P: Prop).P))))
22 \def
23  \lambda (n1: nat).(nat_ind (\lambda (n: nat).(\forall (n2: nat).(or (eq nat 
24 n n2) ((eq nat n n2) \to (\forall (P: Prop).P))))) (\lambda (n2: 
25 nat).(nat_ind (\lambda (n: nat).(or (eq nat O n) ((eq nat O n) \to (\forall 
26 (P: Prop).P)))) (or_introl (eq nat O O) ((eq nat O O) \to (\forall (P: 
27 Prop).P)) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (eq nat O n) 
28 ((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq 
29 nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S 
30 n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match 
31 ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S n) H0) in 
32 (False_ind P H1))))))) n2)) (\lambda (n: nat).(\lambda (H: ((\forall (n2: 
33 nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda 
34 (n2: nat).(nat_ind (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n) 
35 n0) \to (\forall (P: Prop).P)))) (or_intror (eq nat (S n) O) ((eq nat (S n) 
36 O) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat (S n) O)).(\lambda (P: 
37 Prop).(let H1 \def (eq_ind nat (S n) (\lambda (ee: nat).(match ee with [O 
38 \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) 
39 (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to 
40 (\forall (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall 
41 (P: Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall 
42 (P: Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0 
43 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P: 
44 Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S 
45 n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat 
46 (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat 
47 (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P: 
48 Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to 
49 (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P: 
50 Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e with [O 
51 \Rightarrow n | (S n3) \Rightarrow n3])) (S n) (S n0) H2) in (let H4 \def 
52 (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) \to (\forall (P0: 
53 Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 (\lambda (n3: nat).(or 
54 (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: Prop).P0)))) H0 n H3) 
55 in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).
56
57 lemma simpl_plus_r:
58  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) 
59 (plus p n)) \to (eq nat m p))))
60 \def
61  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat 
62 (plus m n) (plus p n))).(simpl_plus_l n m p (eq_ind_r nat (plus m n) (\lambda 
63 (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: 
64 nat).(eq nat n0 (plus n p))) (plus_sym p n) (plus m n) H) (plus n m) 
65 (plus_sym n m)))))).
66
67 lemma minus_Sx_Sy:
68  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
69 \def
70  \lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
71
72 lemma minus_plus_r:
73  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
74 \def
75  \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0: 
76 nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
77
78 lemma plus_permute_2_in_3:
79  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x 
80 y) z) (plus (plus x z) y))))
81 \def
82  \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(eq_ind_r nat (plus x 
83 (plus y z)) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) (eq_ind_r nat 
84 (plus z y) (\lambda (n: nat).(eq nat (plus x n) (plus (plus x z) y))) (eq_ind 
85 nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) 
86 (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z 
87 y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
88
89 lemma plus_permute_2_in_3_assoc:
90  \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n 
91 h) k) (plus n (plus k h)))))
92 \def
93  \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(eq_ind_r nat (plus 
94 (plus n k) h) (\lambda (n0: nat).(eq nat n0 (plus n (plus k h)))) (eq_ind_r 
95 nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0)) 
96 (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k 
97 h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
98
99 lemma plus_O:
100  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat 
101 x O) (eq nat y O))))
102 \def
103  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus 
104 n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda 
105 (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) 
106 H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) 
107 \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq 
108 nat (plus (S n) y) O)).(let H1 \def (match H0 with [refl_equal \Rightarrow 
109 (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n) 
110 y) (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow 
111 True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y O)) H2)))]) in 
112 (H1 (refl_equal nat O))))))) x).
113
114 lemma minus_Sx_SO:
115  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
116 \def
117  \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal 
118 nat x) (minus x O) (minus_n_O x)).
119
120 lemma nat_dec_neg:
121  \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
122 \def
123  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq 
124 nat n j)) (eq nat n j)))) (\lambda (j: nat).(nat_ind (\lambda (n: nat).(or 
125 (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) 
126 (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (not (eq nat O n)) (eq 
127 nat O n))).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) 
128 (\lambda (n: nat).(\lambda (H: ((\forall (j: nat).(or (not (eq nat n j)) (eq 
129 nat n j))))).(\lambda (j: nat).(nat_ind (\lambda (n0: nat).(or (not (eq nat 
130 (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S 
131 n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda (n0: nat).(\lambda (_: (or 
132 (not (eq nat (S n) n0)) (eq nat (S n) n0))).(or_ind (not (eq nat n n0)) (eq 
133 nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda 
134 (H1: (not (eq nat n n0))).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S 
135 n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not 
136 (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H 
137 n0)))) j)))) i).
138
139 lemma neq_eq_e:
140  \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j)) 
141 \to P)) \to ((((eq nat i j) \to P)) \to P))))
142 \def
143  \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not 
144 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def 
145 (nat_dec_neg i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
146
147 lemma le_false:
148  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S 
149 n) m) \to P))))
150 \def
151  \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P: 
152 Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P: 
153 Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match 
154 H0 with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def 
155 (eq_ind nat (S n) (\lambda (e: nat).(match e with [O \Rightarrow False | (S 
156 _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m0 H1) 
157 \Rightarrow (\lambda (H2: (eq nat (S m0) O)).((let H3 \def (eq_ind nat (S m0) 
158 (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow 
159 True])) I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1 
160 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: 
161 nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda 
162 (n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to 
163 ((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) 
164 O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 with [le_n 
165 \Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) 
166 (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow 
167 True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow (\lambda 
168 (H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda (e: 
169 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3) 
170 in (False_ind ((le (S n) m0) \to P) H4)) H2))]) in (H2 (refl_equal nat 
171 O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: Prop).((le (S n) n1) 
172 \to ((le (S n1) (S n)) \to P))))).(\lambda (P: Prop).(\lambda (H1: (le (S n) 
173 (S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1) 
174 (le_S_n (S n1) n H2))))))) n0)))) m).
175
176 lemma le_Sx_x:
177  \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
178 \def
179  \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def 
180 le_Sn_n in (False_ind P (H0 x H))))).
181
182 lemma le_n_pred:
183  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
184 \def
185  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda 
186 (n0: nat).(le (pred n) (pred n0))) (le_n (pred n)) (\lambda (m0: 
187 nat).(\lambda (_: (le n m0)).(\lambda (H1: (le (pred n) (pred m0))).(le_trans 
188 (pred n) (pred m0) m0 H1 (le_pred_n m0))))) m H))).
189
190 lemma minus_le:
191  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
192 \def
193  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n 
194 y) n))) (\lambda (_: nat).(le_O_n O)) (\lambda (n: nat).(\lambda (H: 
195 ((\forall (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda 
196 (n0: nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: 
197 nat).(\lambda (_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow 
198 (minus n l)]) (S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
199
200 lemma le_plus_minus_sym:
201  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) 
202 n))))
203 \def
204  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat 
205 (plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H) 
206 (plus (minus m n) n) (plus_sym (minus m n) n)))).
207
208 lemma le_minus_minus:
209  \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z) 
210 \to (le (minus y x) (minus z x))))))
211 \def
212  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z: 
213 nat).(\lambda (H0: (le y z)).(simpl_le_plus_l x (minus y x) (minus z x) 
214 (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat 
215 z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z 
216 (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
217
218 lemma le_minus_plus:
219  \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat 
220 (minus (plus x y) z) (plus (minus x z) y)))))
221 \def
222  \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to 
223 (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) 
224 (\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H with [le_n 
225 \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: 
226 nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y)))) 
227 (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) 
228 (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq 
229 nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y: 
230 nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O 
231 m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))]) 
232 in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x: 
233 nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus 
234 (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S 
235 z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n 
236 (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def 
237 (match H0 with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 
238 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e with [O \Rightarrow False 
239 | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat (minus (plus O y) 
240 (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) \Rightarrow (\lambda 
241 (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: 
242 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) 
243 in (False_ind ((le (S z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus 
244 (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: 
245 nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus 
246 n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S 
247 n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).
248
249 lemma le_minus:
250  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to 
251 (le x (minus z y)))))
252 \def
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 
256 y))))).
257
258 lemma le_trans_plus_r:
259  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to 
260 (le y z))))
261 \def
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)))).
264
265 lemma lt_x_O:
266  \forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
267 \def
268  \lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let H_y \def 
269 (le_n_O_eq (S x) H) in (let H0 \def (eq_ind nat O (\lambda (ee: nat).(match 
270 ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x) H_y) in 
271 (False_ind P H0))))).
272
273 lemma le_gen_S:
274  \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n: 
275 nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
276 \def
277  \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def 
278 (match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat 
279 (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) 
280 (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S 
281 m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x 
282 H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat 
283 (S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq 
284 nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m) 
285 m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: 
286 nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) 
287 x H1 H0))]) in (H0 (refl_equal nat x))))).
288
289 lemma lt_x_plus_x_Sy:
290  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
291 \def
292  \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n: 
293 nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) 
294 (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
295
296 lemma simpl_lt_plus_r:
297  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m 
298 p)) \to (lt n m))))
299 \def
300  \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus 
301 n p) (plus m p))).(simpl_lt_plus_l n m p (let H0 \def (eq_ind nat (plus n p) 
302 (\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_sym n p)) in (let 
303 H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0 
304 (plus p m) (plus_sym m p)) in H1)))))).
305
306 lemma minus_x_Sy:
307  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S 
308 (minus x (S y))))))
309 \def
310  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to 
311 (eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H: 
312 (lt y O)).(let H0 \def (match H with [le_n \Rightarrow (\lambda (H0: (eq nat 
313 (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e with [O 
314 \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat 
315 (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda 
316 (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: 
317 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) 
318 in (False_ind ((le (S y) m) \to (eq nat (minus O y) (S (minus O (S y))))) 
319 H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (H: 
320 ((\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S (minus n (S 
321 y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to 
322 (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda (_: (lt O (S 
323 n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S n0))) (refl_equal nat 
324 (S n)) (minus n O) (minus_n_O n))) (\lambda (n0: nat).(\lambda (_: (((lt n0 
325 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))).(\lambda 
326 (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0) n H1) in (H n0 H2))))) 
327 y)))) x).
328
329 lemma lt_plus_minus:
330  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus 
331 y (S x)))))))
332 \def
333  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S 
334 x) y H))).
335
336 lemma lt_plus_minus_r:
337  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y 
338 (S x)) x)))))
339 \def
340  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat 
341 (plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x 
342 y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
343
344 lemma minus_x_SO:
345  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
346 \def
347  \lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n: 
348 nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal 
349 nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
350
351 lemma le_x_pred_y:
352  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
353 \def
354  \lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to 
355 (le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def 
356 (match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let H1 \def 
357 (eq_ind nat (S x) (\lambda (e: nat).(match e with [O \Rightarrow False | (S 
358 _) \Rightarrow True])) I O H0) in (False_ind (le x O) H1))) | (le_S m H0) 
359 \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) 
360 (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow 
361 True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0 
362 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt 
363 x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S 
364 n))).(le_S_n x n H0))))) y).
365
366 lemma lt_le_minus:
367  \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
368 \def
369  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S 
370 O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O)) 
371 (plus_sym x (S O)))))).
372
373 lemma lt_le_e:
374  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) 
375 \to ((((le d n) \to P)) \to P))))
376 \def
377  \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n 
378 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in 
379 (or_ind (le d n) (lt n d) P H0 H H1)))))).
380
381 lemma lt_eq_e:
382  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) 
383 \to ((((eq nat x y) \to P)) \to ((le x y) \to P)))))
384 \def
385  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
386 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x 
387 y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
388
389 lemma lt_eq_gt_e:
390  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) 
391 \to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P)))))
392 \def
393  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
394 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x) 
395 \to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda 
396 (H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
397
398 lemma lt_gen_xS:
399  \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2 
400 nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n))))))
401 \def
402  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).((lt n (S 
403 n0)) \to (or (eq nat n O) (ex2 nat (\lambda (m: nat).(eq nat n (S m))) 
404 (\lambda (m: nat).(lt m n0))))))) (\lambda (n: nat).(\lambda (_: (lt O (S 
405 n))).(or_introl (eq nat O O) (ex2 nat (\lambda (m: nat).(eq nat O (S m))) 
406 (\lambda (m: nat).(lt m n))) (refl_equal nat O)))) (\lambda (n: nat).(\lambda 
407 (_: ((\forall (n0: nat).((lt n (S n0)) \to (or (eq nat n O) (ex2 nat (\lambda 
408 (m: nat).(eq nat n (S m))) (\lambda (m: nat).(lt m n0)))))))).(\lambda (n0: 
409 nat).(\lambda (H0: (lt (S n) (S n0))).(or_intror (eq nat (S n) O) (ex2 nat 
410 (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0))) 
411 (ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt 
412 m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
413
414 lemma le_lt_false:
415  \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P: 
416 Prop).P))))
417 \def
418  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt 
419 y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
420
421 lemma lt_neq:
422  \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
423 \def
424  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq 
425 nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in 
426 (lt_n_n y H1))))).
427
428 lemma arith0:
429  \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n) 
430 \to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2))))))
431 \def
432  \lambda (h2: nat).(\lambda (d2: nat).(\lambda (n: nat).(\lambda (H: (le 
433 (plus d2 h2) n)).(\lambda (h1: nat).(eq_ind nat (minus (plus h2 (plus d2 h1)) 
434 h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2 
435 (plus h2 (plus d2 h1)) (le_plus_l h2 (plus d2 h1)) (plus n h1) (eq_ind_r nat 
436 (plus (plus h2 d2) h1) (\lambda (n0: nat).(le n0 (plus n h1))) (eq_ind_r nat 
437 (plus d2 h2) (\lambda (n0: nat).(le (plus n0 h1) (plus n h1))) (le_S_n (plus 
438 (plus d2 h2) h1) (plus n h1) (le_n_S (plus (plus d2 h2) h1) (plus n h1) 
439 (le_plus_plus (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_sym h2 
440 d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1) 
441 (minus_plus h2 (plus d2 h1))))))).
442
443 lemma O_minus:
444  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
445 \def
446  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to 
447 (eq nat (minus n y) O)))) (\lambda (y: nat).(\lambda (_: (le O 
448 y)).(refl_equal nat O))) (\lambda (x0: nat).(\lambda (H: ((\forall (y: 
449 nat).((le x0 y) \to (eq nat (minus x0 y) O))))).(\lambda (y: nat).(nat_ind 
450 (\lambda (n: nat).((le (S x0) n) \to (eq nat (match n with [O \Rightarrow (S 
451 x0) | (S l) \Rightarrow (minus x0 l)]) O))) (\lambda (H0: (le (S x0) 
452 O)).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le x0 
453 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H1: (eq nat O (S 
454 x1))).(\lambda (_: (le x0 x1)).(let H3 \def (eq_ind nat O (\lambda (ee: 
455 nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x1) 
456 H1) in (False_ind (eq nat (S x0) O) H3))))) (le_gen_S x0 O H0))) (\lambda (n: 
457 nat).(\lambda (_: (((le (S x0) n) \to (eq nat (match n with [O \Rightarrow (S 
458 x0) | (S l) \Rightarrow (minus x0 l)]) O)))).(\lambda (H1: (le (S x0) (S 
459 n))).(H n (le_S_n x0 n H1))))) y)))) x).
460
461 lemma minus_minus:
462  \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y) 
463 \to ((eq nat (minus x z) (minus y z)) \to (eq nat x y))))))
464 \def
465  \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).(\forall (y: 
466 nat).((le n x) \to ((le n y) \to ((eq nat (minus x n) (minus y n)) \to (eq 
467 nat x y))))))) (\lambda (x: nat).(\lambda (y: nat).(\lambda (_: (le O 
468 x)).(\lambda (_: (le O y)).(\lambda (H1: (eq nat (minus x O) (minus y 
469 O))).(let H2 \def (eq_ind_r nat (minus x O) (\lambda (n: nat).(eq nat n 
470 (minus y O))) H1 x (minus_n_O x)) in (let H3 \def (eq_ind_r nat (minus y O) 
471 (\lambda (n: nat).(eq nat x n)) H2 y (minus_n_O y)) in H3))))))) (\lambda 
472 (z0: nat).(\lambda (IH: ((\forall (x: nat).(\forall (y: nat).((le z0 x) \to 
473 ((le z0 y) \to ((eq nat (minus x z0) (minus y z0)) \to (eq nat x 
474 y)))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le 
475 (S z0) n) \to ((le (S z0) y) \to ((eq nat (minus n (S z0)) (minus y (S z0))) 
476 \to (eq nat n y)))))) (\lambda (y: nat).(\lambda (H: (le (S z0) O)).(\lambda 
477 (_: (le (S z0) y)).(\lambda (_: (eq nat (minus O (S z0)) (minus y (S 
478 z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le 
479 z0 n)) (eq nat O y) (\lambda (x0: nat).(\lambda (H2: (eq nat O (S 
480 x0))).(\lambda (_: (le z0 x0)).(let H4 \def (eq_ind nat O (\lambda (ee: 
481 nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x0) 
482 H2) in (False_ind (eq nat O y) H4))))) (le_gen_S z0 O H)))))) (\lambda (x0: 
483 nat).(\lambda (_: ((\forall (y: nat).((le (S z0) x0) \to ((le (S z0) y) \to 
484 ((eq nat (minus x0 (S z0)) (minus y (S z0))) \to (eq nat x0 y))))))).(\lambda 
485 (y: nat).(nat_ind (\lambda (n: nat).((le (S z0) (S x0)) \to ((le (S z0) n) 
486 \to ((eq nat (minus (S x0) (S z0)) (minus n (S z0))) \to (eq nat (S x0) 
487 n))))) (\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) O)).(\lambda 
488 (_: (eq nat (minus (S x0) (S z0)) (minus O (S z0)))).(let H_y \def (le_S_n z0 
489 x0 H) in (ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: 
490 nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H2: (eq nat O 
491 (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O (\lambda (ee: 
492 nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x1) 
493 H2) in (False_ind (eq nat (S x0) O) H4))))) (le_gen_S z0 O H0)))))) (\lambda 
494 (y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to ((eq nat 
495 (minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0) y0)))))).(\lambda 
496 (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S y0))).(\lambda (H1: (eq 
497 nat (minus (S x0) (S z0)) (minus (S y0) (S z0)))).(f_equal nat nat S x0 y0 
498 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z).
499
500 lemma plus_plus:
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)))))))))
504 \def
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 (y3: nat).(\forall (y4: nat).((le O z0) \to ((le O z0) \to ((eq 
529 nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) H_y z0 (minus_n_O z0)) 
530 in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (eq_add_S (plus z0 y1) (plus z0 y2) 
531 H1))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2: 
532 nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) (plus 
533 (match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2)) 
534 \to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2: 
535 nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S x3) (S z0))).(\lambda 
536 (H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2))).(let H_y \def (IH O 
537 x3 (S y1)) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n: 
538 nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S 
539 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H_y z0 
540 (minus_n_O z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda (n: 
541 nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus 
542 (minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1)) 
543 (plus_n_Sm z0 y1)) in (let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda 
544 (n: nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus 
545 z0 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 n)))))) H3 (S (plus x3 y1)) 
546 (plus_n_Sm x3 y1)) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1)))))))))))) 
547 x2)) (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall (y1: 
548 nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat 
549 (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2 
550 y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(nat_ind (\lambda (n: 
551 nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S 
552 z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2)) 
553 \to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda (y1: nat).(\lambda 
554 (y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (_: (le O (S 
555 z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))).(let 
556 H_y \def (IH x2 O y1 (S y2)) in (let H2 \def (eq_ind_r nat (minus z0 O) 
557 (\lambda (n: nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) 
558 y1) (plus n (S y2))) \to (eq nat (plus x2 (S y2)) y1))))) H_y z0 (minus_n_O 
559 z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda (n: nat).((le x2 
560 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (eq nat (plus 
561 x2 (S y2)) y1))))) H2 (S (plus z0 y2)) (plus_n_Sm z0 y2)) in (let H4 \def 
562 (eq_ind_r nat (plus x2 (S y2)) (\lambda (n: nat).((le x2 z0) \to ((le O z0) 
563 \to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1))))) 
564 H3 (S (plus x2 y2)) (plus_n_Sm x2 y2)) in (H4 (le_S_n x2 z0 H) (le_O_n z0) 
565 H1)))))))))) (\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall 
566 (y2: nat).((le (S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus 
567 z0 x2) y1) (plus (match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow 
568 (minus z0 l)]) y2)) \to (eq nat (S (plus x2 y2)) (plus x4 
569 y1))))))))).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S 
570 z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0 
571 x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4 
572 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) 
573 x1)))) z).
574
575 lemma le_S_minus:
576  \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to 
577 (le d (S (minus n h))))))
578 \def
579  \lambda (d: nat).(\lambda (h: nat).(\lambda (n: nat).(\lambda (H: (le (plus 
580 d h) n)).(let H0 \def (le_trans d (plus d h) n (le_plus_l d h) H) in (let H1 
581 \def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus n h) h) 
582 (le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S 
583 d (minus n h) (le_minus d n h H))))))).
584
585 lemma lt_x_pred_y:
586  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
587 \def
588  \lambda (x: nat).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((lt x (pred 
589 n)) \to (lt (S x) n))) (\lambda (H: (lt x O)).(lt_x_O x H (lt (S x) O))) 
590 (\lambda (n: nat).(\lambda (_: (((lt x (pred n)) \to (lt (S x) n)))).(\lambda 
591 (H0: (lt x n)).(lt_n_S x n H0)))) y)).
592