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 include "Legacy-1/coq/defs.ma".
20 \forall (A: Set).(\forall (B: Set).(\forall (f: ((A \to B))).(\forall (x:
21 A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
23 \lambda (A: Set).(\lambda (B: Set).(\lambda (f: ((A \to B))).(\lambda (x:
24 A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x (\lambda (a: A).(eq B
25 (f x) (f a))) (refl_equal B (f x)) y H)))))).
31 \forall (A1: Set).(\forall (A2: Set).(\forall (B: Set).(\forall (f: ((A1 \to
32 (A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2: A2).(\forall
33 (y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2) (f y1
36 \lambda (A1: Set).(\lambda (A2: Set).(\lambda (B: Set).(\lambda (f: ((A1 \to
37 (A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda
38 (y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2
39 x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 y2)).(eq_ind
40 A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B (f x1 x2)) y2
47 \forall (A1: Set).(\forall (A2: Set).(\forall (A3: Set).(\forall (B:
48 Set).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1: A1).(\forall
49 (y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3: A3).(\forall (y3:
50 A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2
51 x3) (f y1 y2 y3)))))))))))))))
53 \lambda (A1: Set).(\lambda (A2: Set).(\lambda (A3: Set).(\lambda (B:
54 Set).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1: A1).(\lambda
55 (y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3: A3).(\lambda (y3:
56 A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2 x2 y2)
57 \to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3))))) (\lambda (H0: (eq
58 A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3) \to (eq B (f x1 x2
59 x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 x3 (\lambda (a:
60 A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 x3)) y3 H1)) y2
61 H0)) y1 H)))))))))))).
67 \forall (A: Set).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y
70 \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
71 y)).(eq_ind A x (\lambda (a: A).(eq A a x)) (refl_equal A x) y H)))).
77 \forall (A: Set).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
78 (\forall (y: A).((eq A y x) \to (P y))))))
80 \lambda (A: Set).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda (H:
81 (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) in
82 eq return (\lambda (a: A).(\lambda (_: (eq ? ? a)).(P a))) with [refl_equal
89 \forall (A: Set).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A x y)
90 \to ((eq A y z) \to (eq A x z))))))
92 \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (z: A).(\lambda
93 (H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda (a: A).(eq A x
100 \forall (A: Set).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to (not
103 \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq A x
104 y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a y))
105 (refl_equal A y) x h2)))))).
110 theorem nat_double_ind:
111 \forall (R: ((nat \to (nat \to Prop)))).(((\forall (n: nat).(R O n))) \to
112 (((\forall (n: nat).(R (S n) O))) \to (((\forall (n: nat).(\forall (m:
113 nat).((R n m) \to (R (S n) (S m)))))) \to (\forall (n: nat).(\forall (m:
116 \lambda (R: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (n: nat).(R O
117 n)))).(\lambda (H0: ((\forall (n: nat).(R (S n) O)))).(\lambda (H1: ((\forall
118 (n: nat).(\forall (m: nat).((R n m) \to (R (S n) (S m))))))).(\lambda (n:
119 nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(R n0 m))) H (\lambda (n0:
120 nat).(\lambda (H2: ((\forall (m: nat).(R n0 m)))).(\lambda (m: nat).(nat_ind
121 (\lambda (n1: nat).(R (S n0) n1)) (H0 n0) (\lambda (n1: nat).(\lambda (_: (R
122 (S n0) n1)).(H1 n0 n1 (H2 n1)))) m)))) n))))).
128 \forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
130 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S
131 m))).(f_equal nat nat pred (S n) (S m) H))).
137 \forall (n: nat).(not (eq nat O (S n)))
139 \lambda (n: nat).(\lambda (H: (eq nat O (S n))).(eq_ind nat (S n) (\lambda
140 (n0: nat).(IsSucc n0)) I O (sym_eq nat O (S n) H))).
146 \forall (n: nat).(\forall (m: nat).((not (eq nat n m)) \to (not (eq nat (S
149 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda
150 (H0: (eq nat (S n) (S m))).(H (eq_add_S n m H0))))).
156 \forall (m: nat).(eq nat m (pred (S m)))
158 \lambda (m: nat).(refl_equal nat (pred (S m))).
164 \forall (n: nat).(\forall (m: nat).((lt m n) \to (eq nat n (S (pred n)))))
166 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt m n)).(le_ind (S m)
167 (\lambda (n0: nat).(eq nat n0 (S (pred n0)))) (refl_equal nat (S (pred (S
168 m)))) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (_: (eq nat m0
169 (S (pred m0)))).(refl_equal nat (S (pred (S m0))))))) n H))).
175 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((le m p)
178 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
179 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(le n n0)) H
180 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (le n m0)).(le_S n
181 m0 IHle)))) p H0))))).
187 \forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
189 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(le_trans n (S
190 n) m (le_S n n (le_n n)) H))).
196 \forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
198 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
199 (n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
200 n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
206 \forall (n: nat).(le O n)
208 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le O n0)) (le_n O) (\lambda
209 (n0: nat).(\lambda (IHn: (le O n0)).(le_S O n0 IHn))) n).
215 \forall (n: nat).(\forall (m: nat).((le (S n) (S m)) \to (le n m)))
217 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) (S m))).(le_ind (S
218 n) (\lambda (n0: nat).(le (pred (S n)) (pred n0))) (le_n n) (\lambda (m0:
219 nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S
220 n m0 H0)))) (S m) H))).
226 \forall (n: nat).(not (le (S n) O))
228 \lambda (n: nat).(\lambda (H: (le (S n) O)).(le_ind (S n) (\lambda (n0:
229 nat).(IsSucc n0)) I (\lambda (m: nat).(\lambda (_: (le (S n) m)).(\lambda (_:
230 (IsSucc m)).I))) O H)).
236 \forall (n: nat).(not (le (S n) n))
238 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(not (le (S n0) n0))) (le_Sn_O
239 O) (\lambda (n0: nat).(\lambda (IHn: (not (le (S n0) n0))).(\lambda (H: (le
240 (S (S n0)) (S n0))).(IHn (le_S_n (S n0) n0 H))))) n).
246 \forall (n: nat).(\forall (m: nat).((le n m) \to ((le m n) \to (eq nat n
249 \lambda (n: nat).(\lambda (m: nat).(\lambda (h: (le n m)).(le_ind n (\lambda
250 (n0: nat).((le n0 n) \to (eq nat n n0))) (\lambda (_: (le n n)).(refl_equal
251 nat n)) (\lambda (m0: nat).(\lambda (H: (le n m0)).(\lambda (_: (((le m0 n)
252 \to (eq nat n m0)))).(\lambda (H1: (le (S m0) n)).(False_ind (eq nat n (S
253 m0)) (let H2 \def (le_trans (S m0) n m0 H1 H) in ((let H3 \def (le_Sn_n m0)
254 in (\lambda (H4: (le (S m0) m0)).(H3 H4))) H2))))))) m h))).
260 \forall (n: nat).((le n O) \to (eq nat O n))
262 \lambda (n: nat).(\lambda (H: (le n O)).(le_antisym O n (le_O_n n) H)).
268 \forall (P: ((nat \to (nat \to Prop)))).(((\forall (p: nat).(P O p))) \to
269 (((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p q) \to (P (S p) (S
270 q))))))) \to (\forall (n: nat).(\forall (m: nat).((le n m) \to (P n m))))))
272 \lambda (P: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (p: nat).(P O
273 p)))).(\lambda (H0: ((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p
274 q) \to (P (S p) (S q)))))))).(\lambda (n: nat).(nat_ind (\lambda (n0:
275 nat).(\forall (m: nat).((le n0 m) \to (P n0 m)))) (\lambda (m: nat).(\lambda
276 (_: (le O m)).(H m))) (\lambda (n0: nat).(\lambda (IHn: ((\forall (m:
277 nat).((le n0 m) \to (P n0 m))))).(\lambda (m: nat).(\lambda (Le: (le (S n0)
278 m)).(le_ind (S n0) (\lambda (n1: nat).(P (S n0) n1)) (H0 n0 n0 (le_n n0) (IHn
279 n0 (le_n n0))) (\lambda (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_:
280 (P (S n0) m0)).(H0 n0 m0 (le_trans_S n0 m0 H1) (IHn m0 (le_trans_S n0 m0
281 H1)))))) m Le))))) n)))).
287 \forall (n: nat).(not (lt n n))
295 \forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
297 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_n_S (S n) m
304 \forall (n: nat).(lt n (S n))
306 \lambda (n: nat).(le_n (S n)).
312 \forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
314 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(le_S_n (S
321 \forall (n: nat).(not (lt n O))
329 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((lt m p)
332 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
333 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) (le_S
334 (S n) m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt
335 n m0)).(le_S (S n) m0 IHle)))) p H0))))).
341 \forall (n: nat).(lt O (S n))
343 \lambda (n: nat).(le_n_S O n (le_O_n n)).
349 \forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
351 \lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
357 \forall (n: nat).(\forall (m: nat).((le n m) \to (not (lt m n))))
359 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
360 (n0: nat).(not (lt n0 n))) (lt_n_n n) (\lambda (m0: nat).(\lambda (_: (le n
361 m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(IHle
362 (le_trans_S (S m0) n H1)))))) m H))).
368 \forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
370 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
376 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((lt m p)
379 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
380 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0))
381 (le_n_S n m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle:
382 (lt n m0)).(le_S (S n) m0 IHle)))) p H0))))).
388 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((le m p)
391 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
392 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(lt n n0)) H
393 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (lt n m0)).(le_S
394 (S n) m0 IHle)))) p H0))))).
400 \forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
402 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m
409 \forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
411 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m
418 \forall (n: nat).(\forall (m: nat).((le n m) \to (or (lt n m) (eq nat n m))))
420 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
421 (n0: nat).(or (lt n n0) (eq nat n n0))) (or_intror (lt n n) (eq nat n n)
422 (refl_equal nat n)) (\lambda (m0: nat).(\lambda (H0: (le n m0)).(\lambda (_:
423 (or (lt n m0) (eq nat n m0))).(or_introl (lt n (S m0)) (eq nat n (S m0))
424 (le_n_S n m0 H0))))) m H))).
430 \forall (n: nat).(\forall (m: nat).(or (le n m) (lt m n)))
432 \lambda (n: nat).(\lambda (m: nat).(nat_double_ind (\lambda (n0:
433 nat).(\lambda (n1: nat).(or (le n0 n1) (lt n1 n0)))) (\lambda (n0:
434 nat).(or_introl (le O n0) (lt n0 O) (le_O_n n0))) (\lambda (n0:
435 nat).(or_intror (le (S n0) O) (lt O (S n0)) (lt_le_S O (S n0) (lt_O_Sn n0))))
436 (\lambda (n0: nat).(\lambda (m0: nat).(\lambda (H: (or (le n0 m0) (lt m0
437 n0))).(or_ind (le n0 m0) (lt m0 n0) (or (le (S n0) (S m0)) (lt (S m0) (S
438 n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S
439 n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S
440 m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
446 \forall (n: nat).(eq nat n (plus n O))
448 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (plus n0 O)))
449 (refl_equal nat O) (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0
450 O))).(f_equal nat nat S n0 (plus n0 O) H))) n).
456 \forall (n: nat).(\forall (m: nat).(eq nat (S (plus n m)) (plus n (S m))))
458 \lambda (m: nat).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (S
459 (plus n0 n)) (plus n0 (S n)))) (refl_equal nat (S n)) (\lambda (n0:
460 nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S n)))).(f_equal nat nat
461 S (S (plus n0 n)) (plus n0 (S n)) H))) m)).
467 \forall (n: nat).(\forall (m: nat).(eq nat (plus n m) (plus m n)))
469 \lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(eq nat (plus
470 n0 m) (plus m n0))) (plus_n_O m) (\lambda (y: nat).(\lambda (H: (eq nat (plus
471 y m) (plus m y))).(eq_ind nat (S (plus m y)) (\lambda (n0: nat).(eq nat (S
472 (plus y m)) n0)) (f_equal nat nat S (plus y m) (plus m y) H) (plus m (S y))
473 (plus_n_Sm m y)))) n)).
478 theorem plus_Snm_nSm:
479 \forall (n: nat).(\forall (m: nat).(eq nat (plus (S n) m) (plus n (S m))))
481 \lambda (n: nat).(\lambda (m: nat).(eq_ind_r nat (plus m n) (\lambda (n0:
482 nat).(eq nat (S n0) (plus n (S m)))) (eq_ind_r nat (plus (S m) n) (\lambda
483 (n0: nat).(eq nat (S (plus m n)) n0)) (refl_equal nat (plus (S m) n)) (plus n
484 (S m)) (plus_sym n (S m))) (plus n m) (plus_sym n m))).
489 theorem plus_assoc_l:
490 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus n (plus m
491 p)) (plus (plus n m) p))))
493 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
494 nat).(eq nat (plus n0 (plus m p)) (plus (plus n0 m) p))) (refl_equal nat
495 (plus m p)) (\lambda (n0: nat).(\lambda (H: (eq nat (plus n0 (plus m p))
496 (plus (plus n0 m) p))).(f_equal nat nat S (plus n0 (plus m p)) (plus (plus n0
502 theorem plus_assoc_r:
503 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus (plus n
504 m) p) (plus n (plus m p)))))
506 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(sym_eq nat (plus n
507 (plus m p)) (plus (plus n m) p) (plus_assoc_l n m p)))).
512 theorem simpl_plus_l:
513 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus n m)
514 (plus n p)) \to (eq nat m p))))
516 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(\forall (p:
517 nat).((eq nat (plus n0 m) (plus n0 p)) \to (eq nat m p))))) (\lambda (m:
518 nat).(\lambda (p: nat).(\lambda (H: (eq nat m p)).H))) (\lambda (n0:
519 nat).(\lambda (IHn: ((\forall (m: nat).(\forall (p: nat).((eq nat (plus n0 m)
520 (plus n0 p)) \to (eq nat m p)))))).(\lambda (m: nat).(\lambda (p:
521 nat).(\lambda (H: (eq nat (S (plus n0 m)) (S (plus n0 p)))).(IHn m p (IHn
522 (plus n0 m) (plus n0 p) (f_equal nat nat (plus n0) (plus n0 m) (plus n0 p)
523 (eq_add_S (plus n0 m) (plus n0 p) H))))))))) n).
529 \forall (n: nat).(eq nat n (minus n O))
531 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (minus n0 O)))
532 (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0
533 O))).(refl_equal nat (S n0)))) n).
539 \forall (n: nat).(eq nat O (minus n n))
541 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat O (minus n0 n0)))
542 (refl_equal nat O) (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0
549 \forall (n: nat).(\forall (m: nat).((le m n) \to (eq nat (S (minus n m))
552 \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le m n)).(le_elim_rel
553 (\lambda (n0: nat).(\lambda (n1: nat).(eq nat (S (minus n1 n0)) (minus (S n1)
554 n0)))) (\lambda (p: nat).(f_equal nat nat S (minus p O) p (sym_eq nat p
555 (minus p O) (minus_n_O p)))) (\lambda (p: nat).(\lambda (q: nat).(\lambda (_:
556 (le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match p with [O \Rightarrow
557 (S q) | (S l) \Rightarrow (minus q l)]))).H0)))) m n Le))).
563 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat n (plus m p))
564 \to (eq nat p (minus n m)))))
566 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_double_ind
567 (\lambda (n0: nat).(\lambda (n1: nat).((eq nat n1 (plus n0 p)) \to (eq nat p
568 (minus n1 n0))))) (\lambda (n0: nat).(\lambda (H: (eq nat n0 p)).(eq_ind nat
569 n0 (\lambda (n1: nat).(eq nat p n1)) (sym_eq nat n0 p H) (minus n0 O)
570 (minus_n_O n0)))) (\lambda (n0: nat).(\lambda (H: (eq nat O (S (plus n0
571 p)))).(False_ind (eq nat p O) (let H0 \def H in ((let H1 \def (O_S (plus n0
572 p)) in (\lambda (H2: (eq nat O (S (plus n0 p)))).(H1 H2))) H0))))) (\lambda
573 (n0: nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq
574 nat p (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(H
575 (eq_add_S m0 (plus n0 p) H0)))))) m n))).
581 \forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
583 \lambda (n: nat).(\lambda (m: nat).(sym_eq nat m (minus (plus n m) n)
584 (plus_minus (plus n m) n m (refl_equal nat (plus n m))))).
590 \forall (n: nat).(le (pred n) n)
592 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le (pred n0) n0)) (le_n O)
593 (\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(le_S (pred (S n0)) n0
600 \forall (n: nat).(\forall (m: nat).(le n (plus n m)))
602 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(le n0 (plus
603 n0 m)))) (\lambda (m: nat).(le_O_n m)) (\lambda (n0: nat).(\lambda (IHn:
604 ((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(le_n_S n0 (plus
605 n0 m) (IHn m))))) n).
611 \forall (n: nat).(\forall (m: nat).(le m (plus n m)))
613 \lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(le m (plus
614 n0 m))) (le_n m) (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(le_S m
615 (plus n0 m) H))) n)).
620 theorem simpl_le_plus_l:
621 \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((le (plus p n) (plus p
624 \lambda (p: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (m:
625 nat).((le (plus n n0) (plus n m)) \to (le n0 m))))) (\lambda (n:
626 nat).(\lambda (m: nat).(\lambda (H: (le n m)).H))) (\lambda (p0:
627 nat).(\lambda (IHp: ((\forall (n: nat).(\forall (m: nat).((le (plus p0 n)
628 (plus p0 m)) \to (le n m)))))).(\lambda (n: nat).(\lambda (m: nat).(\lambda
629 (H: (le (S (plus p0 n)) (S (plus p0 m)))).(IHp n m (le_S_n (plus p0 n) (plus
635 theorem le_plus_trans:
636 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le n
639 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
640 m)).(le_trans n m (plus m p) H (le_plus_l m p))))).
646 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le (plus
649 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
650 nat).((le n m) \to (le (plus n0 n) (plus n0 m)))) (\lambda (H: (le n m)).H)
651 (\lambda (p0: nat).(\lambda (IHp: (((le n m) \to (le (plus p0 n) (plus p0
652 m))))).(\lambda (H: (le n m)).(le_n_S (plus p0 n) (plus p0 m) (IHp H)))))
658 theorem le_plus_plus:
659 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
660 n m) \to ((le p q) \to (le (plus n p) (plus m q)))))))
662 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
663 nat).(\lambda (H: (le n m)).(\lambda (H0: (le p q)).(le_ind n (\lambda (n0:
664 nat).(le (plus n p) (plus n0 q))) (le_reg_l p q n H0) (\lambda (m0:
665 nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus m0 q))).(le_S
666 (plus n p) (plus m0 q) H2)))) m H)))))).
671 theorem le_plus_minus:
672 \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus n (minus m
675 \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le n m)).(le_elim_rel
676 (\lambda (n0: nat).(\lambda (n1: nat).(eq nat n1 (plus n0 (minus n1 n0)))))
677 (\lambda (p: nat).(minus_n_O p)) (\lambda (p: nat).(\lambda (q: nat).(\lambda
678 (_: (le p q)).(\lambda (H0: (eq nat q (plus p (minus q p)))).(f_equal nat nat
679 S q (plus p (minus q p)) H0))))) n m Le))).
684 theorem le_plus_minus_r:
685 \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat (plus n (minus m
688 \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(sym_eq nat m
689 (plus n (minus m n)) (le_plus_minus n m H)))).
694 theorem simpl_lt_plus_l:
695 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt (plus p n) (plus p
698 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
699 nat).((lt (plus n0 n) (plus n0 m)) \to (lt n m))) (\lambda (H: (lt n m)).H)
700 (\lambda (p0: nat).(\lambda (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n
701 m)))).(\lambda (H: (lt (S (plus p0 n)) (S (plus p0 m)))).(IHp (le_S_n (S
702 (plus p0 n)) (plus p0 m) H))))) p))).
708 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
711 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
712 nat).((lt n m) \to (lt (plus n0 n) (plus n0 m)))) (\lambda (H: (lt n m)).H)
713 (\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to (lt (plus p0 n) (plus p0
714 m))))).(\lambda (H: (lt n m)).(lt_n_S (plus p0 n) (plus p0 m) (IHp H)))))
721 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
724 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
725 m)).(eq_ind_r nat (plus p n) (\lambda (n0: nat).(lt n0 (plus m p))) (eq_ind_r
726 nat (plus p m) (\lambda (n0: nat).(lt (plus p n) n0)) (nat_ind (\lambda (n0:
727 nat).(lt (plus n0 n) (plus n0 m))) H (\lambda (n0: nat).(\lambda (_: (lt
728 (plus n0 n) (plus n0 m))).(lt_reg_l n m (S n0) H))) p) (plus m p) (plus_sym m
729 p)) (plus n p) (plus_sym n p))))).
734 theorem le_lt_plus_plus:
735 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
736 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
738 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
739 nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(eq_ind_r nat (plus n
740 (S p)) (\lambda (n0: nat).(le n0 (plus m q))) (le_plus_plus n m (S p) q H H0)
741 (plus (S n) p) (plus_Snm_nSm n p))))))).
746 theorem lt_le_plus_plus:
747 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
748 n m) \to ((le p q) \to (lt (plus n p) (plus m q)))))))
750 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
751 nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(le_plus_plus (S n) m
757 theorem lt_plus_plus:
758 \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
759 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
761 \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
762 nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(lt_le_plus_plus n m p q
763 H (lt_le_weak p q H0))))))).
768 theorem well_founded_ltof:
769 \forall (A: Set).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
771 \lambda (A: Set).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n:
772 nat).(nat_ind (\lambda (n0: nat).(\forall (a: A).((lt (f a) n0) \to (Acc A
773 (ltof A f) a)))) (\lambda (a: A).(\lambda (H: (lt (f a) O)).(False_ind (Acc A
774 (ltof A f) a) (let H0 \def H in ((let H1 \def (lt_n_O (f a)) in (\lambda (H2:
775 (lt (f a) O)).(H1 H2))) H0))))) (\lambda (n0: nat).(\lambda (IHn: ((\forall
776 (a: A).((lt (f a) n0) \to (Acc A (ltof A f) a))))).(\lambda (a: A).(\lambda
777 (ltSma: (lt (f a) (S n0))).(Acc_intro A (ltof A f) a (\lambda (b: A).(\lambda
778 (ltfafb: (lt (f b) (f a))).(IHn b (lt_le_trans (f b) (f a) n0 ltfafb
779 (lt_n_Sm_le (f a) n0 ltSma)))))))))) n)) in (\lambda (a: A).(H (S (f a)) a
780 (le_n (S (f a))))))).
788 well_founded_ltof nat (\lambda (m: nat).m).
794 \forall (p: nat).(\forall (P: ((nat \to Prop))).(((\forall (n:
795 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n)))) \to (P p)))
797 \lambda (p: nat).(\lambda (P: ((nat \to Prop))).(\lambda (H: ((\forall (n:
798 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n))))).(Acc_ind nat lt
799 (\lambda (n: nat).(P n)) (\lambda (x: nat).(\lambda (_: ((\forall (y:
800 nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall (y: nat).((lt y
801 x) \to (P y))))).(H x H1)))) p (lt_wf p)))).