((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq
nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S
n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match
-ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I (S n) H0)
-in (False_ind P H1))))))) n2)) (\lambda (n: nat).(\lambda (H: ((\forall (n2:
+ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S n) H0) in
+(False_ind P H1))))))) n2)) (\lambda (n: nat).(\lambda (H: ((\forall (n2:
nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda
(n2: nat).(nat_ind (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n)
n0) \to (\forall (P: Prop).P)))) (or_intror (eq nat (S n) O) ((eq nat (S n)
O) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat (S n) O)).(\lambda (P:
-Prop).(let H1 \def (eq_ind nat (S n) (\lambda (ee: nat).(match ee in nat with
-[O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind P
-H1))))) (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n)
-n0) \to (\forall (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to
-(\forall (P: Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
-(\forall (P: Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r
-nat n0 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to
-(\forall (P: Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq
-nat (S n) (S n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P))))
-(or_introl (eq nat (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P:
-Prop).P)) (refl_equal nat (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to
-(\forall (P: Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S
-n0)) \to (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda
-(P: Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat
-with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n) (S n0) H2) in (let H4
-\def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) \to (\forall (P0:
+Prop).(let H1 \def (eq_ind nat (S n) (\lambda (ee: nat).(match ee with [O
+\Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1)))))
+(\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to
+(\forall (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall
+(P: Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall
+(P: Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0
+(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P:
+Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S
+n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat
+(S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat
+(S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P:
+Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
+(\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P:
+Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e with [O
+\Rightarrow n | (S n3) \Rightarrow n3])) (S n) (S n0) H2) in (let H4 \def
+(eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) \to (\forall (P0:
Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 (\lambda (n3: nat).(or
(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).
(H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O)
H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O)
\to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq
-nat (plus (S n) y) O)).(let H1 \def (match H0 in eq with [refl_equal
-\Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat
-(plus (S n) y) (\lambda (e: nat).(match e in nat with [O \Rightarrow False |
-(S _) \Rightarrow 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).
+nat (plus (S n) y) O)).(let H1 \def (match H0 with [refl_equal \Rightarrow
+(\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n)
+y) (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
+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).
theorem minus_Sx_SO:
\forall (x: nat).(eq nat (minus (S x) (S O)) x)
\lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P:
Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P:
Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match
-H0 in le with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
-(eq_ind nat (S n) (\lambda (e: nat).(match e in nat with [O \Rightarrow False
-| (S _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m0 H1)
+H0 with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
+(eq_ind nat (S n) (\lambda (e: nat).(match e with [O \Rightarrow False | (S
+_) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m0 H1)
\Rightarrow (\lambda (H2: (eq nat (S m0) O)).((let H3 \def (eq_ind nat (S m0)
-(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))])
-in (H1 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0:
+(\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1
+(refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0:
nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda
(n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to
((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n)
-O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 in le with [le_n
+O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 with [le_n
\Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n)
-(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow
-(\lambda (H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda
-(e: nat).(match e in nat with [O \Rightarrow False | (S _) \Rightarrow
-True])) I O H3) in (False_ind ((le (S n) m0) \to P) H4)) H2))]) in (H2
-(refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P:
-Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P:
-Prop).(\lambda (H1: (le (S n) (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).
+(\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow (\lambda
+(H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda (e:
+nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3)
+in (False_ind ((le (S n) m0) \to P) H4)) H2))]) in (H2 (refl_equal nat
+O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: Prop).((le (S n) n1)
+\to ((le (S n1) (S n)) \to P))))).(\lambda (P: Prop).(\lambda (H1: (le (S n)
+(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).
theorem le_Sx_x:
\forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
\def
\lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to
(\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y))))))
-(\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le with
-[le_n \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n:
+(\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H with [le_n
+\Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n:
nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))
(\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O)
(minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq
(minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S
z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n
(S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def
-(match H0 in le with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let
-H2 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e in nat with [O
-\Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat
-(minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1)
-\Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m)
-(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H2) in (False_ind ((le (S z0) m) \to (eq nat (minus
-(plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal
-nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S z0) n) \to (\forall (y:
-nat).(eq nat (minus (plus 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).
+(match H0 with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2
+\def (eq_ind nat (S z0) (\lambda (e: nat).(match e with [O \Rightarrow False
+| (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat (minus (plus O y)
+(S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) \Rightarrow (\lambda
+(H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e:
+nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2)
+in (False_ind ((le (S z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus
+(minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal nat O))))) (\lambda (n:
+nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus
+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).
theorem le_minus:
\forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to
\def
\lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let H_y \def
(le_n_O_eq (S x) H) in (let H0 \def (eq_ind nat O (\lambda (ee: nat).(match
-ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x) H_y)
-in (False_ind P H0))))).
+ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x) H_y) in
+(False_ind P H0))))).
theorem le_gen_S:
\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
\lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def
-(match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind
-nat (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0)))
+(match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat
+(S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0)))
(\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S
m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x
H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat
\def
\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
(eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H:
-(lt y O)).(let H0 \def (match H in le with [le_n \Rightarrow (\lambda (H0:
-(eq nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e
-in nat with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in
-(False_ind (eq nat (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0)
-\Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m)
-(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat (minus O
-y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda
-(n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S
-(minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0
-(S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda (_:
-(lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S n0)))
-(refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0:
-nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S
-n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0)
-n H1) in (H n0 H2))))) y)))) x).
+(lt y O)).(let H0 \def (match H with [le_n \Rightarrow (\lambda (H0: (eq nat
+(S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e with [O
+\Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat
+(minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda
+(H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e:
+nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1)
+in (False_ind ((le (S y) m) \to (eq nat (minus O y) (S (minus O (S y)))))
+H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (H:
+((\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S (minus n (S
+y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to
+(eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda (_: (lt O (S
+n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S n0))) (refl_equal nat
+(S n)) (minus n O) (minus_n_O n))) (\lambda (n0: nat).(\lambda (_: (((lt n0
+(S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))).(\lambda
+(H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0) n H1) in (H n0 H2)))))
+y)))) x).
theorem lt_plus_minus:
\forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus
\def
\lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to
(le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def
-(match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let H1
-\def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat with [O \Rightarrow
-False | (S _) \Rightarrow True])) I O H0) in (False_ind (le x O) H1))) |
-(le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind
-nat (S m) (\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2))
-H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall
-(x: nat).((lt x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0:
-(lt x (S n))).(le_S_n x n H0))))) y).
+(match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let H1 \def
+(eq_ind nat (S x) (\lambda (e: nat).(match e with [O \Rightarrow False | (S
+_) \Rightarrow True])) I O H0) in (False_ind (le x O) H1))) | (le_S m H0)
+\Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m)
+(\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0
+(refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt
+x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S
+n))).(le_S_n x n H0))))) y).
theorem lt_le_minus:
\forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
O)).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le x0
n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H1: (eq nat O (S
x1))).(\lambda (_: (le x0 x1)).(let H3 \def (eq_ind nat O (\lambda (ee:
-nat).(match ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I
-(S x1) H1) in (False_ind (eq nat (S x0) O) H3))))) (le_gen_S x0 O H0)))
-(\lambda (n: nat).(\lambda (_: (((le (S x0) n) \to (eq nat (match n with [O
-\Rightarrow (S 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).
+nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x1)
+H1) in (False_ind (eq nat (S x0) O) H3))))) (le_gen_S x0 O H0))) (\lambda (n:
+nat).(\lambda (_: (((le (S x0) n) \to (eq nat (match n with [O \Rightarrow (S
+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).
theorem minus_minus:
\forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y)
z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le
z0 n)) (eq nat O y) (\lambda (x0: nat).(\lambda (H2: (eq nat O (S
x0))).(\lambda (_: (le z0 x0)).(let H4 \def (eq_ind nat O (\lambda (ee:
-nat).(match ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I
-(S x0) H2) in (False_ind (eq nat O y) H4))))) (le_gen_S z0 O H)))))) (\lambda
-(x0: nat).(\lambda (_: ((\forall (y: nat).((le (S z0) x0) \to ((le (S z0) y)
-\to ((eq nat (minus x0 (S z0)) (minus y (S z0))) \to (eq nat x0
-y))))))).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((le (S z0) (S x0)) \to
-((le (S z0) n) \to ((eq nat (minus (S x0) (S z0)) (minus n (S z0))) \to (eq
-nat (S x0) n))))) (\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0)
-O)).(\lambda (_: (eq nat (minus (S x0) (S z0)) (minus O (S z0)))).(let H_y
-\def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda (n: nat).(eq nat O (S n)))
-(\lambda (n: nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda
-(H2: (eq nat O (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O
-(\lambda (ee: nat).(match ee in nat with [O \Rightarrow True | (S _)
-\Rightarrow False])) I (S x1) H2) in (False_ind (eq nat (S x0) O) H4)))))
-(le_gen_S z0 O H0)))))) (\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0))
-\to ((le (S z0) y0) \to ((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to
-(eq nat (S x0) y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S
-z0) (S y0))).(\lambda (H1: (eq 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).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x0)
+H2) in (False_ind (eq nat O y) H4))))) (le_gen_S z0 O H)))))) (\lambda (x0:
+nat).(\lambda (_: ((\forall (y: nat).((le (S z0) x0) \to ((le (S z0) y) \to
+((eq nat (minus x0 (S z0)) (minus y (S z0))) \to (eq nat x0 y))))))).(\lambda
+(y: nat).(nat_ind (\lambda (n: nat).((le (S z0) (S x0)) \to ((le (S z0) n)
+\to ((eq nat (minus (S x0) (S z0)) (minus n (S z0))) \to (eq nat (S x0)
+n))))) (\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) O)).(\lambda
+(_: (eq nat (minus (S x0) (S z0)) (minus O (S z0)))).(let H_y \def (le_S_n z0
+x0 H) in (ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n:
+nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H2: (eq nat O
+(S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O (\lambda (ee:
+nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x1)
+H2) in (False_ind (eq nat (S x0) O) H4))))) (le_gen_S z0 O H0)))))) (\lambda
+(y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to ((eq nat
+(minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0) y0)))))).(\lambda
+(H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S y0))).(\lambda (H1: (eq
+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).
theorem plus_plus:
\forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1: