-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).
-
-theorem plus_plus:
+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).
+
+lemma plus_plus: