\lambda (A: Set).(\lambda (B: Set).(\lambda (f: ((A \to B))).(\lambda (x:
A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x (\lambda (a: A).(eq B
(f x) (f a))) (refl_equal B (f x)) y H)))))).
\lambda (A: Set).(\lambda (B: Set).(\lambda (f: ((A \to B))).(\lambda (x:
A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x (\lambda (a: A).(eq B
(f x) (f a))) (refl_equal B (f x)) y H)))))).
x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 y2)).(eq_ind
A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B (f x1 x2)) y2
H0)) y1 H))))))))).
x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 y2)).(eq_ind
A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B (f x1 x2)) y2
H0)) y1 H))))))))).
x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 x3 (\lambda (a:
A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 x3)) y3 H1)) y2
H0)) y1 H)))))))))))).
x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 x3 (\lambda (a:
A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 x3)) y3 H1)) y2
H0)) y1 H)))))))))))).
\def
\lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
y)).(eq_ind A x (\lambda (a: A).(eq A a x)) (refl_equal A x) y H)))).
\def
\lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
y)).(eq_ind A x (\lambda (a: A).(eq A a x)) (refl_equal A x) y H)))).
(P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) in
eq return (\lambda (a: A).(\lambda (_: (eq ? ? a)).(P a))) with [refl_equal
\Rightarrow H])))))).
(P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) in
eq return (\lambda (a: A).(\lambda (_: (eq ? ? a)).(P a))) with [refl_equal
\Rightarrow H])))))).
\lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (z: A).(\lambda
(H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda (a: A).(eq A x
a)) H z H0)))))).
\lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (z: A).(\lambda
(H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda (a: A).(eq A x
a)) H z H0)))))).
\lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq A x
y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a y))
(refl_equal A y) x h2)))))).
\lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq A x
y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a y))
(refl_equal A y) x h2)))))).
nat).(\lambda (H2: ((\forall (m: nat).(R n0 m)))).(\lambda (m: nat).(nat_ind
(\lambda (n1: nat).(R (S n0) n1)) (H0 n0) (\lambda (n1: nat).(\lambda (_: (R
(S n0) n1)).(H1 n0 n1 (H2 n1)))) m)))) n))))).
nat).(\lambda (H2: ((\forall (m: nat).(R n0 m)))).(\lambda (m: nat).(nat_ind
(\lambda (n1: nat).(R (S n0) n1)) (H0 n0) (\lambda (n1: nat).(\lambda (_: (R
(S n0) n1)).(H1 n0 n1 (H2 n1)))) m)))) n))))).
theorem eq_add_S:
\forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S
m))).(f_equal nat nat pred (S n) (S m) H))).
theorem eq_add_S:
\forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S
m))).(f_equal nat nat pred (S n) (S m) H))).
theorem O_S:
\forall (n: nat).(not (eq nat O (S n)))
\def
\lambda (n: nat).(\lambda (H: (eq nat O (S n))).(eq_ind nat (S n) (\lambda
(n0: nat).(IsSucc n0)) I O (sym_eq nat O (S n) H))).
theorem O_S:
\forall (n: nat).(not (eq nat O (S n)))
\def
\lambda (n: nat).(\lambda (H: (eq nat O (S n))).(eq_ind nat (S n) (\lambda
(n0: nat).(IsSucc n0)) I O (sym_eq nat O (S n) H))).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda
(H0: (eq nat (S n) (S m))).(H (eq_add_S n m H0))))).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda
(H0: (eq nat (S n) (S m))).(H (eq_add_S n m H0))))).
(\lambda (n0: nat).(eq nat n0 (S (pred n0)))) (refl_equal nat (S (pred (S
m)))) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (_: (eq nat m0
(S (pred m0)))).(refl_equal nat (S (pred (S m0))))))) n H))).
(\lambda (n0: nat).(eq nat n0 (S (pred n0)))) (refl_equal nat (S (pred (S
m)))) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (_: (eq nat m0
(S (pred m0)))).(refl_equal nat (S (pred (S m0))))))) n H))).
m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(le n n0)) H
(\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (le n m0)).(le_S n
m0 IHle)))) p H0))))).
m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(le n n0)) H
(\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (le n m0)).(le_S n
m0 IHle)))) p H0))))).
theorem le_trans_S:
\forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(le_trans n (S
n) m (le_S n n (le_n n)) H))).
theorem le_trans_S:
\forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(le_trans n (S
n) m (le_S n n (le_n n)) H))).
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
(n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
(n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
theorem le_O_n:
\forall (n: nat).(le O n)
\def
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(le O n0)) (le_n O) (\lambda
(n0: nat).(\lambda (IHn: (le O n0)).(le_S O n0 IHn))) n).
theorem le_O_n:
\forall (n: nat).(le O n)
\def
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(le O n0)) (le_n O) (\lambda
(n0: nat).(\lambda (IHn: (le O n0)).(le_S O n0 IHn))) n).
n) (\lambda (n0: nat).(le (pred (S n)) (pred n0))) (le_n n) (\lambda (m0:
nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S
n m0 H0)))) (S m) H))).
n) (\lambda (n0: nat).(le (pred (S n)) (pred n0))) (le_n n) (\lambda (m0:
nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S
n m0 H0)))) (S m) H))).
\lambda (n: nat).(\lambda (H: (le (S n) O)).(le_ind (S n) (\lambda (n0:
nat).(IsSucc n0)) I (\lambda (m: nat).(\lambda (_: (le (S n) m)).(\lambda (_:
(IsSucc m)).I))) O H)).
\lambda (n: nat).(\lambda (H: (le (S n) O)).(le_ind (S n) (\lambda (n0:
nat).(IsSucc n0)) I (\lambda (m: nat).(\lambda (_: (le (S n) m)).(\lambda (_:
(IsSucc m)).I))) O H)).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(not (le (S n0) n0))) (le_Sn_O
O) (\lambda (n0: nat).(\lambda (IHn: (not (le (S n0) n0))).(\lambda (H: (le
(S (S n0)) (S n0))).(IHn (le_S_n (S n0) n0 H))))) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(not (le (S n0) n0))) (le_Sn_O
O) (\lambda (n0: nat).(\lambda (IHn: (not (le (S n0) n0))).(\lambda (H: (le
(S (S n0)) (S n0))).(IHn (le_S_n (S n0) n0 H))))) n).
\to (eq nat n m0)))).(\lambda (H1: (le (S m0) n)).(False_ind (eq nat n (S
m0)) (let H2 \def (le_trans (S m0) n m0 H1 H) in ((let H3 \def (le_Sn_n m0)
in (\lambda (H4: (le (S m0) m0)).(H3 H4))) H2))))))) m h))).
\to (eq nat n m0)))).(\lambda (H1: (le (S m0) n)).(False_ind (eq nat n (S
m0)) (let H2 \def (le_trans (S m0) n m0 H1 H) in ((let H3 \def (le_Sn_n m0)
in (\lambda (H4: (le (S m0) m0)).(H3 H4))) H2))))))) m h))).
theorem le_n_O_eq:
\forall (n: nat).((le n O) \to (eq nat O n))
\def
\lambda (n: nat).(\lambda (H: (le n O)).(le_antisym O n (le_O_n n) H)).
theorem le_n_O_eq:
\forall (n: nat).((le n O) \to (eq nat O n))
\def
\lambda (n: nat).(\lambda (H: (le n O)).(le_antisym O n (le_O_n n) H)).
n0 (le_n n0))) (\lambda (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_:
(P (S n0) m0)).(H0 n0 m0 (le_trans_S n0 m0 H1) (IHn m0 (le_trans_S n0 m0
H1)))))) m Le))))) n)))).
n0 (le_n n0))) (\lambda (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_:
(P (S n0) m0)).(H0 n0 m0 (le_trans_S n0 m0 H1) (IHn m0 (le_trans_S n0 m0
H1)))))) m Le))))) n)))).
theorem lt_n_S:
\forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_n_S (S n) m
H))).
theorem lt_n_S:
\forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_n_S (S n) m
H))).
theorem lt_S_n:
\forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(le_S_n (S
n) m H))).
theorem lt_S_n:
\forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(le_S_n (S
n) m H))).
m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) (le_S
(S n) m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt
n m0)).(le_S (S n) m0 IHle)))) p H0))))).
m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) (le_S
(S n) m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt
n m0)).(le_S (S n) m0 IHle)))) p H0))))).
theorem lt_le_S:
\forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
\def
\lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
theorem lt_le_S:
\forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
\def
\lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
(n0: nat).(not (lt n0 n))) (lt_n_n n) (\lambda (m0: nat).(\lambda (_: (le n
m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(IHle
(le_trans_S (S m0) n H1)))))) m H))).
(n0: nat).(not (lt n0 n))) (lt_n_n n) (\lambda (m0: nat).(\lambda (_: (le n
m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(IHle
(le_trans_S (S m0) n H1)))))) m H))).
theorem le_lt_n_Sm:
\forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
theorem le_lt_n_Sm:
\forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0))
(le_n_S n m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle:
(lt n m0)).(le_S (S n) m0 IHle)))) p H0))))).
m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0))
(le_n_S n m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle:
(lt n m0)).(le_S (S n) m0 IHle)))) p H0))))).
m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(lt n n0)) H
(\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (lt n m0)).(le_S
(S n) m0 IHle)))) p H0))))).
m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(lt n n0)) H
(\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (lt n m0)).(le_S
(S n) m0 IHle)))) p H0))))).
theorem lt_le_weak:
\forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m
H))).
theorem lt_le_weak:
\forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m
H))).
theorem lt_n_Sm_le:
\forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m
H))).
theorem lt_n_Sm_le:
\forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m
H))).
(refl_equal nat n)) (\lambda (m0: nat).(\lambda (H0: (le n m0)).(\lambda (_:
(or (lt n m0) (eq nat n m0))).(or_introl (lt n (S m0)) (eq nat n (S m0))
(le_n_S n m0 H0))))) m H))).
(refl_equal nat n)) (\lambda (m0: nat).(\lambda (H0: (le n m0)).(\lambda (_:
(or (lt n m0) (eq nat n m0))).(or_introl (lt n (S m0)) (eq nat n (S m0))
(le_n_S n m0 H0))))) m H))).
n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S
n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S
m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S
n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S
m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (plus n0 O)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0
O))).(f_equal nat nat S n0 (plus n0 O) H))) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (plus n0 O)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0
O))).(f_equal nat nat S n0 (plus n0 O) H))) n).
(plus n0 n)) (plus n0 (S n)))) (refl_equal nat (S n)) (\lambda (n0:
nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S n)))).(f_equal nat nat
S (S (plus n0 n)) (plus n0 (S n)) H))) m)).
(plus n0 n)) (plus n0 (S n)))) (refl_equal nat (S n)) (\lambda (n0:
nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S n)))).(f_equal nat nat
S (S (plus n0 n)) (plus n0 (S n)) H))) m)).
y m) (plus m y))).(eq_ind nat (S (plus m y)) (\lambda (n0: nat).(eq nat (S
(plus y m)) n0)) (f_equal nat nat S (plus y m) (plus m y) H) (plus m (S y))
(plus_n_Sm m y)))) n)).
y m) (plus m y))).(eq_ind nat (S (plus m y)) (\lambda (n0: nat).(eq nat (S
(plus y m)) n0)) (f_equal nat nat S (plus y m) (plus m y) H) (plus m (S y))
(plus_n_Sm m y)))) n)).
nat).(eq nat (S n0) (plus n (S m)))) (eq_ind_r nat (plus (S m) n) (\lambda
(n0: nat).(eq nat (S (plus m n)) n0)) (refl_equal nat (plus (S m) n)) (plus n
(S m)) (plus_sym n (S m))) (plus n m) (plus_sym n m))).
nat).(eq nat (S n0) (plus n (S m)))) (eq_ind_r nat (plus (S m) n) (\lambda
(n0: nat).(eq nat (S (plus m n)) n0)) (refl_equal nat (plus (S m) n)) (plus n
(S m)) (plus_sym n (S m))) (plus n m) (plus_sym n m))).
(plus m p)) (\lambda (n0: nat).(\lambda (H: (eq nat (plus n0 (plus m p))
(plus (plus n0 m) p))).(f_equal nat nat S (plus n0 (plus m p)) (plus (plus n0
m) p) H))) n))).
(plus m p)) (\lambda (n0: nat).(\lambda (H: (eq nat (plus n0 (plus m p))
(plus (plus n0 m) p))).(f_equal nat nat S (plus n0 (plus m p)) (plus (plus n0
m) p) H))) n))).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(sym_eq nat (plus n
(plus m p)) (plus (plus n m) p) (plus_assoc_l n m p)))).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(sym_eq nat (plus n
(plus m p)) (plus (plus n m) p) (plus_assoc_l n m p)))).
nat).(\lambda (H: (eq nat (S (plus n0 m)) (S (plus n0 p)))).(IHn m p (IHn
(plus n0 m) (plus n0 p) (f_equal nat nat (plus n0) (plus n0 m) (plus n0 p)
(eq_add_S (plus n0 m) (plus n0 p) H))))))))) n).
nat).(\lambda (H: (eq nat (S (plus n0 m)) (S (plus n0 p)))).(IHn m p (IHn
(plus n0 m) (plus n0 p) (f_equal nat nat (plus n0) (plus n0 m) (plus n0 p)
(eq_add_S (plus n0 m) (plus n0 p) H))))))))) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (minus n0 O)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0
O))).(refl_equal nat (S n0)))) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (minus n0 O)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0
O))).(refl_equal nat (S n0)))) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat O (minus n0 n0)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0
n0))).IHn)) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat O (minus n0 n0)))
(refl_equal nat O) (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0
n0))).IHn)) n).
(minus p O) (minus_n_O p)))) (\lambda (p: nat).(\lambda (q: nat).(\lambda (_:
(le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match p with [O \Rightarrow
(S q) | (S l) \Rightarrow (minus q l)]))).H0)))) m n Le))).
(minus p O) (minus_n_O p)))) (\lambda (p: nat).(\lambda (q: nat).(\lambda (_:
(le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match p with [O \Rightarrow
(S q) | (S l) \Rightarrow (minus q l)]))).H0)))) m n Le))).
(n0: nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq
nat p (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(H
(eq_add_S m0 (plus n0 p) H0)))))) m n))).
(n0: nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq
nat p (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(H
(eq_add_S m0 (plus n0 p) H0)))))) m n))).
theorem minus_plus:
\forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
\def
\lambda (n: nat).(\lambda (m: nat).(sym_eq nat m (minus (plus n m) n)
(plus_minus (plus n m) n m (refl_equal nat (plus n m))))).
theorem minus_plus:
\forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
\def
\lambda (n: nat).(\lambda (m: nat).(sym_eq nat m (minus (plus n m) n)
(plus_minus (plus n m) n m (refl_equal nat (plus n m))))).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(le (pred n0) n0)) (le_n O)
(\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(le_S (pred (S n0)) n0
(le_n n0)))) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(le (pred n0) n0)) (le_n O)
(\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(le_S (pred (S n0)) n0
(le_n n0)))) n).
n0 m)))) (\lambda (m: nat).(le_O_n m)) (\lambda (n0: nat).(\lambda (IHn:
((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(le_n_S n0 (plus
n0 m) (IHn m))))) n).
n0 m)))) (\lambda (m: nat).(le_O_n m)) (\lambda (n0: nat).(\lambda (IHn:
((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(le_n_S n0 (plus
n0 m) (IHn m))))) n).
\lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(le m (plus
n0 m))) (le_n m) (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(le_S m
(plus n0 m) H))) n)).
\lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(le m (plus
n0 m))) (le_n m) (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(le_S m
(plus n0 m) H))) n)).
(plus p0 m)) \to (le n m)))))).(\lambda (n: nat).(\lambda (m: nat).(\lambda
(H: (le (S (plus p0 n)) (S (plus p0 m)))).(IHp n m (le_S_n (plus p0 n) (plus
p0 m) H))))))) p).
(plus p0 m)) \to (le n m)))))).(\lambda (n: nat).(\lambda (m: nat).(\lambda
(H: (le (S (plus p0 n)) (S (plus p0 m)))).(IHp n m (le_S_n (plus p0 n) (plus
p0 m) H))))))) p).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
m)).(le_trans n m (plus m p) H (le_plus_l m p))))).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
m)).(le_trans n m (plus m p) H (le_plus_l m p))))).
(\lambda (p0: nat).(\lambda (IHp: (((le n m) \to (le (plus p0 n) (plus p0
m))))).(\lambda (H: (le n m)).(le_n_S (plus p0 n) (plus p0 m) (IHp H)))))
p))).
(\lambda (p0: nat).(\lambda (IHp: (((le n m) \to (le (plus p0 n) (plus p0
m))))).(\lambda (H: (le n m)).(le_n_S (plus p0 n) (plus p0 m) (IHp H)))))
p))).
nat).(le (plus n p) (plus n0 q))) (le_reg_l p q n H0) (\lambda (m0:
nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus m0 q))).(le_S
(plus n p) (plus m0 q) H2)))) m H)))))).
nat).(le (plus n p) (plus n0 q))) (le_reg_l p q n H0) (\lambda (m0:
nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus m0 q))).(le_S
(plus n p) (plus m0 q) H2)))) m H)))))).
(\lambda (p: nat).(minus_n_O p)) (\lambda (p: nat).(\lambda (q: nat).(\lambda
(_: (le p q)).(\lambda (H0: (eq nat q (plus p (minus q p)))).(f_equal nat nat
S q (plus p (minus q p)) H0))))) n m Le))).
(\lambda (p: nat).(minus_n_O p)) (\lambda (p: nat).(\lambda (q: nat).(\lambda
(_: (le p q)).(\lambda (H0: (eq nat q (plus p (minus q p)))).(f_equal nat nat
S q (plus p (minus q p)) H0))))) n m Le))).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(sym_eq nat m
(plus n (minus m n)) (le_plus_minus n m H)))).
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(sym_eq nat m
(plus n (minus m n)) (le_plus_minus n m H)))).
(\lambda (p0: nat).(\lambda (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n
m)))).(\lambda (H: (lt (S (plus p0 n)) (S (plus p0 m)))).(IHp (le_S_n (S
(plus p0 n)) (plus p0 m) H))))) p))).
(\lambda (p0: nat).(\lambda (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n
m)))).(\lambda (H: (lt (S (plus p0 n)) (S (plus p0 m)))).(IHp (le_S_n (S
(plus p0 n)) (plus p0 m) H))))) p))).
(\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to (lt (plus p0 n) (plus p0
m))))).(\lambda (H: (lt n m)).(lt_n_S (plus p0 n) (plus p0 m) (IHp H)))))
p))).
(\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to (lt (plus p0 n) (plus p0
m))))).(\lambda (H: (lt n m)).(lt_n_S (plus p0 n) (plus p0 m) (IHp H)))))
p))).
nat).(lt (plus n0 n) (plus n0 m))) H (\lambda (n0: nat).(\lambda (_: (lt
(plus n0 n) (plus n0 m))).(lt_reg_l n m (S n0) H))) p) (plus m p) (plus_sym m
p)) (plus n p) (plus_sym n p))))).
nat).(lt (plus n0 n) (plus n0 m))) H (\lambda (n0: nat).(\lambda (_: (lt
(plus n0 n) (plus n0 m))).(lt_reg_l n m (S n0) H))) p) (plus m p) (plus_sym m
p)) (plus n p) (plus_sym n p))))).
nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(eq_ind_r nat (plus n
(S p)) (\lambda (n0: nat).(le n0 (plus m q))) (le_plus_plus n m (S p) q H H0)
(plus (S n) p) (plus_Snm_nSm n p))))))).
nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(eq_ind_r nat (plus n
(S p)) (\lambda (n0: nat).(le n0 (plus m q))) (le_plus_plus n m (S p) q H H0)
(plus (S n) p) (plus_Snm_nSm n p))))))).
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(le_plus_plus (S n) m
p q H H0)))))).
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(le_plus_plus (S n) m
p q H H0)))))).
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(lt_le_plus_plus n m p q
H (lt_le_weak p q H0))))))).
\lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(lt_le_plus_plus n m p q
H (lt_le_weak p q H0))))))).
(ltfafb: (lt (f b) (f a))).(IHn b (lt_le_trans (f b) (f a) n0 ltfafb
(lt_n_Sm_le (f a) n0 ltSma)))))))))) n)) in (\lambda (a: A).(H (S (f a)) a
(le_n (S (f a))))))).
(ltfafb: (lt (f b) (f a))).(IHn b (lt_le_trans (f b) (f a) n0 ltfafb
(lt_n_Sm_le (f a) n0 ltSma)))))))))) n)) in (\lambda (a: A).(H (S (f a)) a
(le_n (S (f a))))))).
(\lambda (n: nat).(P n)) (\lambda (x: nat).(\lambda (_: ((\forall (y:
nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall (y: nat).((lt y
x) \to (P y))))).(H x H1)))) p (lt_wf p)))).
(\lambda (n: nat).(P n)) (\lambda (x: nat).(\lambda (_: ((\forall (y:
nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall (y: nat).((lt y
x) \to (P y))))).(H x H1)))) p (lt_wf p)))).