(eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: Prop).P0)))) H0 n H3)
in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).
(eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: Prop).P0)))) H0 n H3)
in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n)
(plus p n)) \to (eq nat m p))))
\def
\forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n)
(plus p n)) \to (eq nat m p))))
\def
\forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
\def
\lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
\forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
\def
\lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
\forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
\def
\lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0:
nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
\forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
\def
\lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0:
nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
\forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x
y) z) (plus (plus x z) y))))
\def
\forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x
y) z) (plus (plus x z) y))))
\def
(refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z
y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
(refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z
y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
\forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n
h) k) (plus n (plus k h)))))
\def
\forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n
h) k) (plus n (plus k h)))))
\def
(refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k
h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
(refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k
h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y O)) H2)))]) in
(H1 (refl_equal nat O))))))) x).
True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y O)) H2)))]) in
(H1 (refl_equal nat O))))))) x).
\forall (x: nat).(eq nat (minus (S x) (S O)) x)
\def
\lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal
nat x) (minus x O) (minus_n_O x)).
\forall (x: nat).(eq nat (minus (S x) (S O)) x)
\def
\lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal
nat x) (minus x O) (minus_n_O x)).
\forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
\def
\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq
\forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
\def
\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq
\forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j))
\to P)) \to ((((eq nat i j) \to P)) \to P))))
\def
\forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j))
\to P)) \to ((((eq nat i j) \to P)) \to P))))
\def
(eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def
(nat_dec_neg i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
(eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def
(nat_dec_neg i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
(S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1)
(le_S_n (S n1) n H2))))))) n0)))) m).
(S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1)
(le_S_n (S n1) n H2))))))) n0)))) m).
\forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
\def
\lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def
le_Sn_n in (False_ind P (H0 x H))))).
\forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
\def
\lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def
le_Sn_n in (False_ind P (H0 x H))))).
\forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
\forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
nat).(\lambda (_: (le n m0)).(\lambda (H1: (le (pred n) (pred m0))).(le_trans
(pred n) (pred m0) m0 H1 (le_pred_n m0))))) m H))).
nat).(\lambda (_: (le n m0)).(\lambda (H1: (le (pred n) (pred m0))).(le_trans
(pred n) (pred m0) m0 H1 (le_pred_n m0))))) m H))).
\forall (x: nat).(\forall (y: nat).(le (minus x y) x))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n
\forall (x: nat).(\forall (y: nat).(le (minus x y) x))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n
nat).(\lambda (_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow
(minus n l)]) (S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
nat).(\lambda (_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow
(minus n l)]) (S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
(plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H)
(plus (minus m n) n) (plus_sym (minus m n) n)))).
(plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H)
(plus (minus m n) n) (plus_sym (minus m n) n)))).
\forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z)
\to (le (minus y x) (minus z x))))))
\def
\forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z)
\to (le (minus y x) (minus z x))))))
\def
z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z
(le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z
(le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
\forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat
(minus (plus x y) z) (plus (minus x z) y)))))
\def
\forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat
(minus (plus x y) z) (plus (minus x z) y)))))
\def
n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S
n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).
n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S
n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).
\forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to
(le y z))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus
x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
\forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to
(le y z))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus
x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
\forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
\def
\lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let H_y \def
\forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
\def
\lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let H_y \def
\forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n:
nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
\def
\forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n:
nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
\def
nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2))))
x H1 H0))]) in (H0 (refl_equal nat x))))).
nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2))))
x H1 H0))]) in (H0 (refl_equal nat x))))).
\forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
\def
\lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n:
nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x))
(le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
\forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
\def
\lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n:
nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x))
(le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0
(plus p m) (plus_sym m p)) in H1)))))).
H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0
(plus p m) (plus_sym m p)) in H1)))))).
\forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus
y (S x)))))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S
x) y H))).
\forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus
y (S x)))))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S
x) y H))).
(plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x
y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
(plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x
y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
\forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
\def
\lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n:
nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal
nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
\forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
\def
\lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n:
nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal
nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
\forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
\def
\lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to
\forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
\def
\lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to
\forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S
O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O))
(plus_sym x (S O)))))).
\forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S
O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O))
(plus_sym x (S O)))))).
\forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P))
\to ((((le d n) \to P)) \to P))))
\def
\forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P))
\to ((((le d n) \to P)) \to P))))
\def
d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in
(or_ind (le d n) (lt n d) P H0 H H1)))))).
d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in
(or_ind (le d n) (lt n d) P H0 H H1)))))).
\forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
\to ((((eq nat x y) \to P)) \to ((le x y) \to P)))))
\def
\forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
\to ((((eq nat x y) \to P)) \to ((le x y) \to P)))))
\def
y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x
y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x
y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
\forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
\to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P)))))
\def
\forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
\to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P)))))
\def
\to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda
(H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
\to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda
(H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
\forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2
nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n))))))
\def
\forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2
nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n))))))
\def
(ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt
m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
(ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt
m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
\forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P:
Prop).P))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt
y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
\forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P:
Prop).P))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt
y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
\forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq
nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in
(lt_n_n y H1))))).
\forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
\def
\lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq
nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in
(lt_n_n y H1))))).
\forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n)
\to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2))))))
\def
\forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n)
\to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2))))))
\def
d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1)
(minus_plus h2 (plus d2 h1))))))).
d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1)
(minus_plus h2 (plus d2 h1))))))).
\forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to
\forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to
x0) | (S l) \Rightarrow (minus x0 l)]) O)))).(\lambda (H1: (le (S x0) (S
n))).(H n (le_S_n x0 n H1))))) y)))) x).
x0) | (S l) \Rightarrow (minus x0 l)]) O)))).(\lambda (H1: (le (S x0) (S
n))).(H n (le_S_n x0 n H1))))) y)))) x).
\forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y)
\to ((eq nat (minus x z) (minus y z)) \to (eq nat x y))))))
\def
\forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y)
\to ((eq nat (minus x z) (minus y z)) \to (eq nat x y))))))
\def
nat (minus (S x0) (S z0)) (minus (S y0) (S z0)))).(f_equal nat nat S x0 y0
(IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z).
nat (minus (S x0) (S z0)) (minus (S y0) (S z0)))).(f_equal nat nat S x0 y0
(IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z).
\forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1:
nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z
x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1)))))))))
\forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1:
nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z
x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1)))))))))
\forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to
(le d (S (minus n h))))))
\def
\forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to
(le d (S (minus n h))))))
\def
(le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S
d (minus n h) (le_minus d n h H))))))).
(le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S
d (minus n h) (le_minus d n h H))))))).
\forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
\def
\lambda (x: nat).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((lt x (pred
\forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
\def
\lambda (x: nat).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((lt x (pred