update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_1 / ext / arith.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma b/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma
index 637a865983c21346706b1fcb04c711d5c1c8fe93..724a34747372f80cc491fbc63a85f22a9d59db06 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma
@@ -16,854 +16,577 @@
 
 include "ground_1/preamble.ma".
 
 
 include "ground_1/preamble.ma".
 

-theorem nat_dec:
+lemma nat_dec:

  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 
 (\forall (P: Prop).P))))
 \def
  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 
 (\forall (P: Prop).P))))
 \def

- \lambda (n1: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (n2: nat).(let 
-TMP_1 \def (eq nat n n2) in (let TMP_2 \def ((eq nat n n2) \to (\forall (P: 
-Prop).P)) in (or TMP_1 TMP_2))))) in (let TMP_18 \def (\lambda (n2: nat).(let 
-TMP_6 \def (\lambda (n: nat).(let TMP_4 \def (eq nat O n) in (let TMP_5 \def 
-((eq nat O n) \to (\forall (P: Prop).P)) in (or TMP_4 TMP_5)))) in (let TMP_7 
-\def (eq nat O O) in (let TMP_8 \def ((eq nat O O) \to (\forall (P: Prop).P)) 
-in (let TMP_9 \def (refl_equal nat O) in (let TMP_10 \def (or_introl TMP_7 
-TMP_8 TMP_9) in (let TMP_17 \def (\lambda (n: nat).(\lambda (_: (or (eq nat O 
-n) ((eq nat O n) \to (\forall (P: Prop).P)))).(let TMP_11 \def (S n) in (let 
-TMP_12 \def (eq nat O TMP_11) in (let TMP_13 \def ((eq nat O (S n)) \to 
-(\forall (P: Prop).P)) in (let TMP_16 \def (\lambda (H0: (eq nat O (S 
-n))).(\lambda (P: Prop).(let TMP_14 \def (\lambda (ee: nat).(match ee with [O 
-\Rightarrow True | (S _) \Rightarrow False])) in (let TMP_15 \def (S n) in 
-(let H1 \def (eq_ind nat O TMP_14 I TMP_15 H0) in (False_ind P H1)))))) in 
-(or_intror TMP_12 TMP_13 TMP_16))))))) in (nat_ind TMP_6 TMP_10 TMP_17 
-n2)))))))) in (let TMP_71 \def (\lambda (n: nat).(\lambda (H: ((\forall (n2: 
+ \lambda (n1: nat).(nat_ind (\lambda (n: nat).(\forall (n2: nat).(or (eq nat 
+n n2) ((eq nat n n2) \to (\forall (P: Prop).P))))) (\lambda (n2: 
+nat).(nat_ind (\lambda (n: nat).(or (eq nat O n) ((eq nat O n) \to (\forall 
+(P: Prop).P)))) (or_introl (eq nat O O) ((eq nat O O) \to (\forall (P: 
+Prop).P)) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (eq nat O n) 
+((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 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 
 nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda 

-(n2: nat).(let TMP_22 \def (\lambda (n0: nat).(let TMP_19 \def (S n) in (let 
-TMP_20 \def (eq nat TMP_19 n0) in (let TMP_21 \def ((eq nat (S n) n0) \to 
-(\forall (P: Prop).P)) in (or TMP_20 TMP_21))))) in (let TMP_23 \def (S n) in 
-(let TMP_24 \def (eq nat TMP_23 O) in (let TMP_25 \def ((eq nat (S n) O) \to 
-(\forall (P: Prop).P)) in (let TMP_28 \def (\lambda (H0: (eq nat (S n) 
-O)).(\lambda (P: Prop).(let TMP_26 \def (S n) in (let TMP_27 \def (\lambda 
-(ee: nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow True])) in 
-(let H1 \def (eq_ind nat TMP_26 TMP_27 I O H0) in (False_ind P H1)))))) in 
-(let TMP_29 \def (or_intror TMP_24 TMP_25 TMP_28) in (let TMP_70 \def 
+(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 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 
 (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to 

-(\forall (P: Prop).P)))).(let TMP_30 \def (eq nat n n0) in (let TMP_31 \def 
-((eq nat n n0) \to (\forall (P: Prop).P)) in (let TMP_32 \def (S n) in (let 
-TMP_33 \def (S n0) in (let TMP_34 \def (eq nat TMP_32 TMP_33) in (let TMP_35 
-\def ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_36 \def 
-(or TMP_34 TMP_35) in (let TMP_53 \def (\lambda (H1: (eq nat n n0)).(let 
-TMP_40 \def (\lambda (n3: nat).(let TMP_37 \def (S n) in (let TMP_38 \def (eq 
-nat TMP_37 n3) in (let TMP_39 \def ((eq nat (S n) n3) \to (\forall (P: 
-Prop).P)) in (or TMP_38 TMP_39))))) in (let H2 \def (eq_ind_r nat n0 TMP_40 
-H0 n H1) in (let TMP_45 \def (\lambda (n3: nat).(let TMP_41 \def (S n) in 
-(let TMP_42 \def (S n3) in (let TMP_43 \def (eq nat TMP_41 TMP_42) in (let 
-TMP_44 \def ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)) in (or TMP_43 
-TMP_44)))))) in (let TMP_46 \def (S n) in (let TMP_47 \def (S n) in (let 
-TMP_48 \def (eq nat TMP_46 TMP_47) in (let TMP_49 \def ((eq nat (S n) (S n)) 
-\to (\forall (P: Prop).P)) in (let TMP_50 \def (S n) in (let TMP_51 \def 
-(refl_equal nat TMP_50) in (let TMP_52 \def (or_introl TMP_48 TMP_49 TMP_51) 
-in (eq_ind nat n TMP_45 TMP_52 n0 H1)))))))))))) in (let TMP_68 \def (\lambda 
-(H1: (((eq nat n n0) \to (\forall (P: Prop).P)))).(let TMP_54 \def (S n) in 
-(let TMP_55 \def (S n0) in (let TMP_56 \def (eq nat TMP_54 TMP_55) in (let 
-TMP_57 \def ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_67 
-\def (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P: Prop).(let TMP_58 \def 
-(\lambda (e: nat).(match e with [O \Rightarrow n | (S n3) \Rightarrow n3])) 
-in (let TMP_59 \def (S n) in (let TMP_60 \def (S n0) in (let H3 \def (f_equal 
-nat nat TMP_58 TMP_59 TMP_60 H2) in (let TMP_61 \def (\lambda (n3: nat).((eq 
-nat n n3) \to (\forall (P0: Prop).P0))) in (let H4 \def (eq_ind_r nat n0 
-TMP_61 H1 n H3) in (let TMP_65 \def (\lambda (n3: nat).(let TMP_62 \def (S n) 
-in (let TMP_63 \def (eq nat TMP_62 n3) in (let TMP_64 \def ((eq nat (S n) n3) 
-\to (\forall (P0: Prop).P0)) in (or TMP_63 TMP_64))))) in (let H5 \def 
-(eq_ind_r nat n0 TMP_65 H0 n H3) in (let TMP_66 \def (refl_equal nat n) in 
-(H4 TMP_66 P)))))))))))) in (or_intror TMP_56 TMP_57 TMP_67))))))) in (let 
-TMP_69 \def (H n0) in (or_ind TMP_30 TMP_31 TMP_36 TMP_53 TMP_68 
-TMP_69))))))))))))) in (nat_ind TMP_22 TMP_29 TMP_70 n2))))))))))) in 
-(nat_ind TMP_3 TMP_18 TMP_71 n1)))).
-
-theorem simpl_plus_r:
+(\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).
+
+lemma simpl_plus_r:

  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) 
 (plus p n)) \to (eq nat m p))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat 
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) 
 (plus p n)) \to (eq nat m p))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat 

-(plus m n) (plus p n))).(let TMP_1 \def (plus m n) in (let TMP_3 \def 
-(\lambda (n0: nat).(let TMP_2 \def (plus n p) in (eq nat n0 TMP_2))) in (let 
-TMP_4 \def (plus p n) in (let TMP_6 \def (\lambda (n0: nat).(let TMP_5 \def 
-(plus n p) in (eq nat n0 TMP_5))) in (let TMP_7 \def (plus_sym p n) in (let 
-TMP_8 \def (plus m n) in (let TMP_9 \def (eq_ind_r nat TMP_4 TMP_6 TMP_7 
-TMP_8 H) in (let TMP_10 \def (plus n m) in (let TMP_11 \def (plus_sym n m) in 
-(let TMP_12 \def (eq_ind_r nat TMP_1 TMP_3 TMP_9 TMP_10 TMP_11) in 
-(simpl_plus_l n m p TMP_12)))))))))))))).
-
-theorem minus_Sx_Sy:
+(plus m n) (plus p n))).(simpl_plus_l n m p (eq_ind_r nat (plus m n) (\lambda 
+(n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: 
+nat).(eq nat n0 (plus n p))) (plus_sym p n) (plus m n) H) (plus n m) 
+(plus_sym n m)))))).
+
+lemma minus_Sx_Sy:

  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
 \def
  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
 \def

- \lambda (x: nat).(\lambda (y: nat).(let TMP_1 \def (minus x y) in 
-(refl_equal nat TMP_1))).
+ \lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).

 
 

-theorem minus_plus_r:
+lemma minus_plus_r:

  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
 \def
  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
 \def

- \lambda (m: nat).(\lambda (n: nat).(let TMP_1 \def (plus n m) in (let TMP_3 
-\def (\lambda (n0: nat).(let TMP_2 \def (minus n0 n) in (eq nat TMP_2 m))) in 
-(let TMP_4 \def (minus_plus n m) in (let TMP_5 \def (plus m n) in (let TMP_6 
-\def (plus_sym m n) in (eq_ind_r nat TMP_1 TMP_3 TMP_4 TMP_5 TMP_6))))))).
+ \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))).

 
 

-theorem plus_permute_2_in_3:
+lemma plus_permute_2_in_3:

  \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

- \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(let TMP_1 \def (plus y 
-z) in (let TMP_2 \def (plus x TMP_1) in (let TMP_5 \def (\lambda (n: 
-nat).(let TMP_3 \def (plus x z) in (let TMP_4 \def (plus TMP_3 y) in (eq nat 
-n TMP_4)))) in (let TMP_6 \def (plus z y) in (let TMP_10 \def (\lambda (n: 
-nat).(let TMP_7 \def (plus x n) in (let TMP_8 \def (plus x z) in (let TMP_9 
-\def (plus TMP_8 y) in (eq nat TMP_7 TMP_9))))) in (let TMP_11 \def (plus x 
-z) in (let TMP_12 \def (plus TMP_11 y) in (let TMP_15 \def (\lambda (n: 
-nat).(let TMP_13 \def (plus x z) in (let TMP_14 \def (plus TMP_13 y) in (eq 
-nat n TMP_14)))) in (let TMP_16 \def (plus x z) in (let TMP_17 \def (plus 
-TMP_16 y) in (let TMP_18 \def (refl_equal nat TMP_17) in (let TMP_19 \def 
-(plus z y) in (let TMP_20 \def (plus x TMP_19) in (let TMP_21 \def 
-(plus_assoc_r x z y) in (let TMP_22 \def (eq_ind nat TMP_12 TMP_15 TMP_18 
-TMP_20 TMP_21) in (let TMP_23 \def (plus y z) in (let TMP_24 \def (plus_sym y 
-z) in (let TMP_25 \def (eq_ind_r nat TMP_6 TMP_10 TMP_22 TMP_23 TMP_24) in 
-(let TMP_26 \def (plus x y) in (let TMP_27 \def (plus TMP_26 z) in (let 
-TMP_28 \def (plus_assoc_r x y z) in (eq_ind_r nat TMP_2 TMP_5 TMP_25 TMP_27 
-TMP_28)))))))))))))))))))))))).
-
-theorem plus_permute_2_in_3_assoc:
+ \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(eq_ind_r nat (plus x 
+(plus y z)) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) (eq_ind_r nat 
+(plus z y) (\lambda (n: nat).(eq nat (plus x n) (plus (plus x z) y))) (eq_ind 
+nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) 
+(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)))).
+
+lemma plus_permute_2_in_3_assoc:

  \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

- \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(let TMP_1 \def (plus n 
-k) in (let TMP_2 \def (plus TMP_1 h) in (let TMP_5 \def (\lambda (n0: 
-nat).(let TMP_3 \def (plus k h) in (let TMP_4 \def (plus n TMP_3) in (eq nat 
-n0 TMP_4)))) in (let TMP_6 \def (plus n k) in (let TMP_7 \def (plus TMP_6 h) 
-in (let TMP_10 \def (\lambda (n0: nat).(let TMP_8 \def (plus n k) in (let 
-TMP_9 \def (plus TMP_8 h) in (eq nat TMP_9 n0)))) in (let TMP_11 \def (plus n 
-k) in (let TMP_12 \def (plus TMP_11 h) in (let TMP_13 \def (refl_equal nat 
-TMP_12) in (let TMP_14 \def (plus k h) in (let TMP_15 \def (plus n TMP_14) in 
-(let TMP_16 \def (plus_assoc_l n k h) in (let TMP_17 \def (eq_ind_r nat TMP_7 
-TMP_10 TMP_13 TMP_15 TMP_16) in (let TMP_18 \def (plus n h) in (let TMP_19 
-\def (plus TMP_18 k) in (let TMP_20 \def (plus_permute_2_in_3 n h k) in 
-(eq_ind_r nat TMP_2 TMP_5 TMP_17 TMP_19 TMP_20))))))))))))))))))).
-
-theorem plus_O:
+ \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(eq_ind_r nat (plus 
+(plus n k) h) (\lambda (n0: nat).(eq nat n0 (plus n (plus k h)))) (eq_ind_r 
+nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0)) 
+(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)))).
+
+lemma plus_O:

  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat 
 x O) (eq nat y O))))
 \def
  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat 
 x O) (eq nat y O))))
 \def

- \lambda (x: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (y: nat).((eq 
-nat (plus n y) O) \to (let TMP_1 \def (eq nat n O) in (let TMP_2 \def (eq nat 
-y O) in (land TMP_1 TMP_2)))))) in (let TMP_7 \def (\lambda (y: nat).(\lambda 
-(H: (eq nat (plus O y) O)).(let TMP_4 \def (eq nat O O) in (let TMP_5 \def 
-(eq nat y O) in (let TMP_6 \def (refl_equal nat O) in (conj TMP_4 TMP_5 TMP_6 
-H)))))) in (let TMP_16 \def (\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 with 
-[refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let TMP_8 
-\def (S n) in (let TMP_9 \def (plus TMP_8 y) in (let TMP_10 \def (\lambda (e: 
-nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) in (let 
-H2 \def (eq_ind nat TMP_9 TMP_10 I O H1) in (let TMP_11 \def (S n) in (let 
-TMP_12 \def (eq nat TMP_11 O) in (let TMP_13 \def (eq nat y O) in (let TMP_14 
-\def (land TMP_12 TMP_13) in (False_ind TMP_14 H2))))))))))]) in (let TMP_15 
-\def (refl_equal nat O) in (H1 TMP_15))))))) in (nat_ind TMP_3 TMP_7 TMP_16 
-x)))).
-
-theorem minus_Sx_SO:
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus 
+n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda 
+(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 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).
+
+lemma minus_Sx_SO:

  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
 \def
  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
 \def

- \lambda (x: nat).(let TMP_1 \def (\lambda (n: nat).(eq nat n x)) in (let 
-TMP_2 \def (refl_equal nat x) in (let TMP_3 \def (minus x O) in (let TMP_4 
-\def (minus_n_O x) in (eq_ind nat x TMP_1 TMP_2 TMP_3 TMP_4))))).
+ \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)).

 
 

-theorem nat_dec_neg:
+lemma nat_dec_neg:

  \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
 \def
  \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
 \def

- \lambda (i: nat).(let TMP_4 \def (\lambda (n: nat).(\forall (j: nat).(let 
-TMP_1 \def (eq nat n j) in (let TMP_2 \def (not TMP_1) in (let TMP_3 \def (eq 
-nat n j) in (or TMP_2 TMP_3)))))) in (let TMP_21 \def (\lambda (j: nat).(let 
-TMP_8 \def (\lambda (n: nat).(let TMP_5 \def (eq nat O n) in (let TMP_6 \def 
-(not TMP_5) in (let TMP_7 \def (eq nat O n) in (or TMP_6 TMP_7))))) in (let 
-TMP_9 \def (eq nat O O) in (let TMP_10 \def (not TMP_9) in (let TMP_11 \def 
-(eq nat O O) in (let TMP_12 \def (refl_equal nat O) in (let TMP_13 \def 
-(or_intror TMP_10 TMP_11 TMP_12) in (let TMP_20 \def (\lambda (n: 
-nat).(\lambda (_: (or (not (eq nat O n)) (eq nat O n))).(let TMP_14 \def (S 
-n) in (let TMP_15 \def (eq nat O TMP_14) in (let TMP_16 \def (not TMP_15) in 
-(let TMP_17 \def (S n) in (let TMP_18 \def (eq nat O TMP_17) in (let TMP_19 
-\def (O_S n) in (or_introl TMP_16 TMP_18 TMP_19))))))))) in (nat_ind TMP_8 
-TMP_13 TMP_20 j))))))))) in (let TMP_68 \def (\lambda (n: nat).(\lambda (H: 
-((\forall (j: nat).(or (not (eq nat n j)) (eq nat n j))))).(\lambda (j: 
-nat).(let TMP_27 \def (\lambda (n0: nat).(let TMP_22 \def (S n) in (let 
-TMP_23 \def (eq nat TMP_22 n0) in (let TMP_24 \def (not TMP_23) in (let 
-TMP_25 \def (S n) in (let TMP_26 \def (eq nat TMP_25 n0) in (or TMP_24 
-TMP_26))))))) in (let TMP_28 \def (S n) in (let TMP_29 \def (eq nat TMP_28 O) 
-in (let TMP_30 \def (not TMP_29) in (let TMP_31 \def (S n) in (let TMP_32 
-\def (eq nat TMP_31 O) in (let TMP_33 \def (S n) in (let TMP_34 \def (O_S n) 
-in (let TMP_35 \def (sym_not_eq nat O TMP_33 TMP_34) in (let TMP_36 \def 
-(or_introl TMP_30 TMP_32 TMP_35) in (let TMP_67 \def (\lambda (n0: 
-nat).(\lambda (_: (or (not (eq nat (S n) n0)) (eq nat (S n) n0))).(let TMP_37 
-\def (eq nat n n0) in (let TMP_38 \def (not TMP_37) in (let TMP_39 \def (eq 
-nat n n0) in (let TMP_40 \def (S n) in (let TMP_41 \def (S n0) in (let TMP_42 
-\def (eq nat TMP_40 TMP_41) in (let TMP_43 \def (not TMP_42) in (let TMP_44 
-\def (S n) in (let TMP_45 \def (S n0) in (let TMP_46 \def (eq nat TMP_44 
-TMP_45) in (let TMP_47 \def (or TMP_43 TMP_46) in (let TMP_56 \def (\lambda 
-(H1: (not (eq nat n n0))).(let TMP_48 \def (S n) in (let TMP_49 \def (S n0) 
-in (let TMP_50 \def (eq nat TMP_48 TMP_49) in (let TMP_51 \def (not TMP_50) 
-in (let TMP_52 \def (S n) in (let TMP_53 \def (S n0) in (let TMP_54 \def (eq 
-nat TMP_52 TMP_53) in (let TMP_55 \def (not_eq_S n n0 H1) in (or_introl 
-TMP_51 TMP_54 TMP_55)))))))))) in (let TMP_65 \def (\lambda (H1: (eq nat n 
-n0)).(let TMP_57 \def (S n) in (let TMP_58 \def (S n0) in (let TMP_59 \def 
-(eq nat TMP_57 TMP_58) in (let TMP_60 \def (not TMP_59) in (let TMP_61 \def 
-(S n) in (let TMP_62 \def (S n0) in (let TMP_63 \def (eq nat TMP_61 TMP_62) 
-in (let TMP_64 \def (f_equal nat nat S n n0 H1) in (or_intror TMP_60 TMP_63 
-TMP_64)))))))))) in (let TMP_66 \def (H n0) in (or_ind TMP_38 TMP_39 TMP_47 
-TMP_56 TMP_65 TMP_66))))))))))))))))) in (nat_ind TMP_27 TMP_36 TMP_67 
-j))))))))))))))) in (nat_ind TMP_4 TMP_21 TMP_68 i)))).
-
-theorem neq_eq_e:
+ \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq 
+nat n j)) (eq nat n j)))) (\lambda (j: nat).(nat_ind (\lambda (n: nat).(or 
+(not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) 
+(refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (not (eq nat O n)) (eq 
+nat O n))).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) 
+(\lambda (n: nat).(\lambda (H: ((\forall (j: nat).(or (not (eq nat n j)) (eq 
+nat n j))))).(\lambda (j: nat).(nat_ind (\lambda (n0: nat).(or (not (eq nat 
+(S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S 
+n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda (n0: nat).(\lambda (_: (or 
+(not (eq nat (S n) n0)) (eq nat (S n) n0))).(or_ind (not (eq nat n n0)) (eq 
+nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda 
+(H1: (not (eq nat n n0))).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S 
+n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not 
+(eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H 
+n0)))) j)))) i).
+
+lemma neq_eq_e:

  \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
  \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not 
 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \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
  \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not 
 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def 

-(nat_dec_neg i j) in (let TMP_1 \def (eq nat i j) in (let TMP_2 \def (not 
-TMP_1) in (let TMP_3 \def (eq nat i j) in (or_ind TMP_2 TMP_3 P H H0 
-o))))))))).
+(nat_dec_neg i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).

 
 

-theorem le_false:
+lemma le_false:

  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S 
 n) m) \to P))))
 \def
  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S 
 n) m) \to P))))
 \def

- \lambda (m: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (n0: 
-nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P))))) in (let 
-TMP_9 \def (\lambda (n: nat).(\lambda (P: Prop).(\lambda (_: (le O 
-n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 with [le_n \Rightarrow 
-(\lambda (H1: (eq nat (S n) O)).(let TMP_6 \def (S n) in (let TMP_7 \def 
+ \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 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 with [O \Rightarrow False | (S _) \Rightarrow 
 (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow 

-True])) in (let H2 \def (eq_ind nat TMP_6 TMP_7 I O H1) in (False_ind P 
-H2))))) | (le_S m0 H1) \Rightarrow (\lambda (H2: (eq nat (S m0) O)).(let 
-TMP_2 \def (S m0) in (let TMP_3 \def (\lambda (e: nat).(match e with [O 
-\Rightarrow False | (S _) \Rightarrow True])) in (let H3 \def (eq_ind nat 
-TMP_2 TMP_3 I O H2) in (let TMP_4 \def ((le (S n) m0) \to P) in (let TMP_5 
-\def (False_ind TMP_4 H3) in (TMP_5 H1)))))))]) in (let TMP_8 \def 
-(refl_equal nat O) in (H1 TMP_8))))))) in (let TMP_23 \def (\lambda (n: 
-nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le 
-(S n0) n) \to P)))))).(\lambda (n0: nat).(let TMP_10 \def (\lambda (n1: 
-nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P)))) in 
-(let TMP_18 \def (\lambda (P: Prop).(\lambda (H0: (le (S 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 TMP_15 \def (S n) in (let TMP_16 \def (\lambda (e: 
-nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) in (let 
-H3 \def (eq_ind nat TMP_15 TMP_16 I O H2) in (False_ind P H3))))) | (le_S m0 
-H2) \Rightarrow (\lambda (H3: (eq nat (S m0) O)).(let TMP_11 \def (S m0) in 
-(let TMP_12 \def (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) 
-\Rightarrow True])) in (let H4 \def (eq_ind nat TMP_11 TMP_12 I O H3) in (let 
-TMP_13 \def ((le (S n) m0) \to P) in (let TMP_14 \def (False_ind TMP_13 H4) 
-in (TMP_14 H2)))))))]) in (let TMP_17 \def (refl_equal nat O) in (H2 
-TMP_17)))))) in (let TMP_22 \def (\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))).(let TMP_19 \def (le_S_n n n1 H1) in (let TMP_20 \def (S n1) in (let 
-TMP_21 \def (le_S_n TMP_20 n H2) in (H n1 P TMP_19 TMP_21))))))))) in 
-(nat_ind TMP_10 TMP_18 TMP_22 n0))))))) in (nat_ind TMP_1 TMP_9 TMP_23 m)))).
-
-theorem le_Sx_x:
+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 with [le_n 
+\Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) 
+(\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).
+
+lemma le_Sx_x:

  \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 
  \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 (let TMP_1 \def (H0 x H) in (False_ind P TMP_1))))).
+le_Sn_n in (False_ind P (H0 x H))))).

 
 

-theorem le_n_pred:
+lemma le_n_pred:

  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
 \def
  \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)).(let TMP_3 \def 
-(\lambda (n0: nat).(let TMP_1 \def (pred n) in (let TMP_2 \def (pred n0) in 
-(le TMP_1 TMP_2)))) in (let TMP_4 \def (pred n) in (let TMP_5 \def (le_n 
-TMP_4) in (let TMP_9 \def (\lambda (m0: nat).(\lambda (_: (le n m0)).(\lambda 
-(H1: (le (pred n) (pred m0))).(let TMP_6 \def (pred n) in (let TMP_7 \def 
-(pred m0) in (let TMP_8 \def (le_pred_n m0) in (le_trans TMP_6 TMP_7 m0 H1 
-TMP_8))))))) in (le_ind n TMP_3 TMP_5 TMP_9 m H))))))).
+ \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda 
+(n0: nat).(le (pred n) (pred n0))) (le_n (pred n)) (\lambda (m0: 
+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))).

 
 

-theorem minus_le:
+lemma minus_le:

  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
 \def
  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
 \def

- \lambda (x: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (y: nat).(let 
-TMP_1 \def (minus n y) in (le TMP_1 n)))) in (let TMP_3 \def (\lambda (_: 
-nat).(le_O_n O)) in (let TMP_13 \def (\lambda (n: nat).(\lambda (H: ((\forall 
-(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(let TMP_7 \def (\lambda 
-(n0: nat).(let TMP_4 \def (S n) in (let TMP_5 \def (minus TMP_4 n0) in (let 
-TMP_6 \def (S n) in (le TMP_5 TMP_6))))) in (let TMP_8 \def (S n) in (let 
-TMP_9 \def (le_n TMP_8) in (let TMP_12 \def (\lambda (n0: nat).(\lambda (_: 
-(le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)]) (S 
-n))).(let TMP_10 \def (minus n n0) in (let TMP_11 \def (H n0) in (le_S TMP_10 
-n TMP_11))))) in (nat_ind TMP_7 TMP_9 TMP_12 y)))))))) in (nat_ind TMP_2 
-TMP_3 TMP_13 x)))).
-
-theorem le_plus_minus_sym:
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n 
+y) n))) (\lambda (_: nat).(le_O_n O)) (\lambda (n: nat).(\lambda (H: 
+((\forall (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda 
+(n0: nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: 
+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).
+
+lemma le_plus_minus_sym:

  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) 
 n))))
 \def
  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) 
 n))))
 \def

- \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(let TMP_1 \def 
-(minus m n) in (let TMP_2 \def (plus n TMP_1) in (let TMP_3 \def (\lambda 
-(n0: nat).(eq nat m n0)) in (let TMP_4 \def (le_plus_minus n m H) in (let 
-TMP_5 \def (minus m n) in (let TMP_6 \def (plus TMP_5 n) in (let TMP_7 \def 
-(minus m n) in (let TMP_8 \def (plus_sym TMP_7 n) in (eq_ind_r nat TMP_2 
-TMP_3 TMP_4 TMP_6 TMP_8))))))))))).
+ \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat 
+(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)))).

 
 

-theorem le_minus_minus:
+lemma le_minus_minus:

  \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
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z: 
  \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
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z: 

-nat).(\lambda (H0: (le y z)).(let TMP_1 \def (minus y x) in (let TMP_2 \def 
-(minus z x) in (let TMP_5 \def (\lambda (n: nat).(let TMP_3 \def (minus z x) 
-in (let TMP_4 \def (plus x TMP_3) in (le n TMP_4)))) in (let TMP_6 \def 
-(\lambda (n: nat).(le y n)) in (let TMP_7 \def (minus z x) in (let TMP_8 \def 
-(plus x TMP_7) in (let TMP_9 \def (le_trans x y z H H0) in (let TMP_10 \def 
-(le_plus_minus_r x z TMP_9) in (let TMP_11 \def (eq_ind_r nat z TMP_6 H0 
-TMP_8 TMP_10) in (let TMP_12 \def (minus y x) in (let TMP_13 \def (plus x 
-TMP_12) in (let TMP_14 \def (le_plus_minus_r x y H) in (let TMP_15 \def 
-(eq_ind_r nat y TMP_5 TMP_11 TMP_13 TMP_14) in (simpl_le_plus_l x TMP_1 TMP_2 
-TMP_15)))))))))))))))))).
-
-theorem le_minus_plus:
+nat).(\lambda (H0: (le y z)).(simpl_le_plus_l x (minus y x) (minus z x) 
+(eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat 
+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))))))).
+
+lemma le_minus_plus:

  \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

- \lambda (z: nat).(let TMP_5 \def (\lambda (n: nat).(\forall (x: nat).((le n 
-x) \to (\forall (y: nat).(let TMP_1 \def (plus x y) in (let TMP_2 \def (minus 
-TMP_1 n) in (let TMP_3 \def (minus x n) in (let TMP_4 \def (plus TMP_3 y) in 
-(eq nat TMP_2 TMP_4))))))))) in (let TMP_29 \def (\lambda (x: nat).(\lambda 
-(H: (le O x)).(let H0 \def (match H with [le_n \Rightarrow (\lambda (H0: (eq 
-nat O x)).(let TMP_20 \def (\lambda (n: nat).(\forall (y: nat).(let TMP_16 
-\def (plus n y) in (let TMP_17 \def (minus TMP_16 O) in (let TMP_18 \def 
-(minus n O) in (let TMP_19 \def (plus TMP_18 y) in (eq nat TMP_17 
-TMP_19))))))) in (let TMP_27 \def (\lambda (y: nat).(let TMP_21 \def (minus O 
-O) in (let TMP_22 \def (plus TMP_21 y) in (let TMP_23 \def (plus O y) in (let 
-TMP_24 \def (minus TMP_23 O) in (let TMP_25 \def (plus O y) in (let TMP_26 
-\def (minus_n_O TMP_25) in (sym_eq nat TMP_22 TMP_24 TMP_26)))))))) in 
-(eq_ind nat O TMP_20 TMP_27 x H0)))) | (le_S m H0) \Rightarrow (\lambda (H1: 
-(eq nat (S m) x)).(let TMP_6 \def (S m) in (let TMP_11 \def (\lambda (n: 
-nat).((le O m) \to (\forall (y: nat).(let TMP_7 \def (plus n y) in (let TMP_8 
-\def (minus TMP_7 O) in (let TMP_9 \def (minus n O) in (let TMP_10 \def (plus 
-TMP_9 y) in (eq nat TMP_8 TMP_10)))))))) in (let TMP_15 \def (\lambda (_: (le 
-O m)).(\lambda (y: nat).(let TMP_12 \def (S m) in (let TMP_13 \def (minus 
-TMP_12 O) in (let TMP_14 \def (plus TMP_13 y) in (refl_equal nat TMP_14)))))) 
-in (eq_ind nat TMP_6 TMP_11 TMP_15 x H1 H0)))))]) in (let TMP_28 \def 
-(refl_equal nat x) in (H0 TMP_28))))) in (let TMP_60 \def (\lambda (z0: 
-nat).(\lambda (H: ((\forall (x: nat).((le z0 x) \to (\forall (y: nat).(eq nat 
-(minus (plus x y) z0) (plus (minus x z0) y))))))).(\lambda (x: nat).(let 
-TMP_36 \def (\lambda (n: nat).((le (S z0) n) \to (\forall (y: nat).(let 
-TMP_30 \def (plus n y) in (let TMP_31 \def (S z0) in (let TMP_32 \def (minus 
-TMP_30 TMP_31) in (let TMP_33 \def (S z0) in (let TMP_34 \def (minus n 
-TMP_33) in (let TMP_35 \def (plus TMP_34 y) in (eq nat TMP_32 
-TMP_35)))))))))) in (let TMP_57 \def (\lambda (H0: (le (S z0) O)).(\lambda 
-(y: nat).(let H1 \def (match H0 with [le_n \Rightarrow (\lambda (H1: (eq nat 
-(S z0) O)).(let TMP_47 \def (S z0) in (let TMP_48 \def (\lambda (e: 
-nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) in (let 
-H2 \def (eq_ind nat TMP_47 TMP_48 I O H1) in (let TMP_49 \def (plus O y) in 
-(let TMP_50 \def (S z0) in (let TMP_51 \def (minus TMP_49 TMP_50) in (let 
-TMP_52 \def (S z0) in (let TMP_53 \def (minus O TMP_52) in (let TMP_54 \def 
-(plus TMP_53 y) in (let TMP_55 \def (eq nat TMP_51 TMP_54) in (False_ind 
-TMP_55 H2)))))))))))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) 
-O)).(let TMP_37 \def (S m) in (let TMP_38 \def (\lambda (e: nat).(match e 
-with [O \Rightarrow False | (S _) \Rightarrow True])) in (let H3 \def (eq_ind 
-nat TMP_37 TMP_38 I O H2) in (let TMP_45 \def ((le (S z0) m) \to (let TMP_39 
-\def (plus O y) in (let TMP_40 \def (S z0) in (let TMP_41 \def (minus TMP_39 
-TMP_40) in (let TMP_42 \def (S z0) in (let TMP_43 \def (minus O TMP_42) in 
-(let TMP_44 \def (plus TMP_43 y) in (eq nat TMP_41 TMP_44)))))))) in (let 
-TMP_46 \def (False_ind TMP_45 H3) in (TMP_46 H1)))))))]) in (let TMP_56 \def 
-(refl_equal nat O) in (H1 TMP_56))))) in (let TMP_59 \def (\lambda (n: 
+ \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 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 
+nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y: 
+nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O 
+m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))]) 
+in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x: 
+nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus 
+(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 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 
 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).(let TMP_58 \def (le_S_n z0 n H1) in (H n TMP_58 
-y)))))) in (nat_ind TMP_36 TMP_57 TMP_59 x))))))) in (nat_ind TMP_5 TMP_29 
-TMP_60 z)))).
+n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).

 
 

-theorem le_minus:
+lemma le_minus:

  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to 
 (le x (minus z y)))))
 \def
  \lambda (x: nat).(\lambda (z: nat).(\lambda (y: nat).(\lambda (H: (le (plus 
  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to 
 (le x (minus z y)))))
 \def
  \lambda (x: nat).(\lambda (z: nat).(\lambda (y: nat).(\lambda (H: (le (plus 

-x y) z)).(let TMP_1 \def (plus x y) in (let TMP_2 \def (minus TMP_1 y) in 
-(let TMP_4 \def (\lambda (n: nat).(let TMP_3 \def (minus z y) in (le n 
-TMP_3))) in (let TMP_5 \def (plus x y) in (let TMP_6 \def (le_plus_r x y) in 
-(let TMP_7 \def (le_minus_minus y TMP_5 TMP_6 z H) in (let TMP_8 \def 
-(minus_plus_r x y) in (eq_ind nat TMP_2 TMP_4 TMP_7 x TMP_8))))))))))).
+x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z 
+y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x 
+y))))).

 
 

-theorem le_trans_plus_r:
+lemma le_trans_plus_r:

  \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 
  \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)).(let TMP_1 \def (plus x y) in (let TMP_2 \def (le_plus_r x y) in 
-(le_trans y TMP_1 z TMP_2 H)))))).
+x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).

 
 

-theorem lt_x_O:
+lemma lt_x_O:

  \forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
 \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 TMP_1 
-\def (S x) in (let H_y \def (le_n_O_eq TMP_1 H) in (let TMP_2 \def (\lambda 
-(ee: nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) in 
-(let TMP_3 \def (S x) in (let H0 \def (eq_ind nat O TMP_2 I TMP_3 H_y) in 
-(False_ind P H0)))))))).
+ \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 with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x) H_y) in 
+(False_ind P H0))))).

 
 

-theorem le_gen_S:
+lemma 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 
  \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 with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(let TMP_16 
-\def (S m) in (let TMP_20 \def (\lambda (n: nat).(let TMP_18 \def (\lambda 
-(n0: nat).(let TMP_17 \def (S n0) in (eq nat n TMP_17))) in (let TMP_19 \def 
-(\lambda (n0: nat).(le m n0)) in (ex2 nat TMP_18 TMP_19)))) in (let TMP_23 
-\def (\lambda (n: nat).(let TMP_21 \def (S m) in (let TMP_22 \def (S n) in 
-(eq nat TMP_21 TMP_22)))) in (let TMP_24 \def (\lambda (n: nat).(le m n)) in 
-(let TMP_25 \def (S m) in (let TMP_26 \def (refl_equal nat TMP_25) in (let 
-TMP_27 \def (le_n m) in (let TMP_28 \def (ex_intro2 nat TMP_23 TMP_24 m 
-TMP_26 TMP_27) in (eq_ind nat TMP_16 TMP_20 TMP_28 x H0)))))))))) | (le_S m0 
-H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(let TMP_1 \def (S m0) in 
-(let TMP_5 \def (\lambda (n: nat).((le (S m) m0) \to (let TMP_3 \def (\lambda 
-(n0: nat).(let TMP_2 \def (S n0) in (eq nat n TMP_2))) in (let TMP_4 \def 
-(\lambda (n0: nat).(le m n0)) in (ex2 nat TMP_3 TMP_4))))) in (let TMP_15 
-\def (\lambda (H2: (le (S m) m0)).(let TMP_8 \def (\lambda (n: nat).(let 
-TMP_6 \def (S m0) in (let TMP_7 \def (S n) in (eq nat TMP_6 TMP_7)))) in (let 
-TMP_9 \def (\lambda (n: nat).(le m n)) in (let TMP_10 \def (S m0) in (let 
-TMP_11 \def (refl_equal nat TMP_10) in (let TMP_12 \def (S m) in (let TMP_13 
-\def (le_S TMP_12 m0 H2) in (let TMP_14 \def (le_S_n m m0 TMP_13) in 
-(ex_intro2 nat TMP_8 TMP_9 m0 TMP_11 TMP_14))))))))) in (eq_ind nat TMP_1 
-TMP_5 TMP_15 x H1 H0)))))]) in (let TMP_29 \def (refl_equal nat x) in (H0 
-TMP_29))))).
-
-theorem lt_x_plus_x_Sy:
+(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 
+(S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq 
+nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m) 
+m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: 
+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))))).
+
+lemma lt_x_plus_x_Sy:

  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
 \def
  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
 \def

- \lambda (x: nat).(\lambda (y: nat).(let TMP_1 \def (S y) in (let TMP_2 \def 
-(plus TMP_1 x) in (let TMP_3 \def (\lambda (n: nat).(lt x n)) in (let TMP_4 
-\def (S x) in (let TMP_5 \def (plus y x) in (let TMP_6 \def (S TMP_5) in (let 
-TMP_7 \def (S x) in (let TMP_8 \def (plus y x) in (let TMP_9 \def (S TMP_8) 
-in (let TMP_10 \def (plus y x) in (let TMP_11 \def (le_plus_r y x) in (let 
-TMP_12 \def (le_n_S x TMP_10 TMP_11) in (let TMP_13 \def (le_n_S TMP_7 TMP_9 
-TMP_12) in (let TMP_14 \def (le_S_n TMP_4 TMP_6 TMP_13) in (let TMP_15 \def 
-(S y) in (let TMP_16 \def (plus x TMP_15) in (let TMP_17 \def (S y) in (let 
-TMP_18 \def (plus_sym x TMP_17) in (eq_ind_r nat TMP_2 TMP_3 TMP_14 TMP_16 
-TMP_18)))))))))))))))))))).
-
-theorem simpl_lt_plus_r:
+ \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)))).
+
+lemma simpl_lt_plus_r:

  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m 
 p)) \to (lt n m))))
 \def
  \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus 
  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m 
 p)) \to (lt n m))))
 \def
  \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus 

-n p) (plus m p))).(let TMP_1 \def (plus n p) in (let TMP_3 \def (\lambda (n0: 
-nat).(let TMP_2 \def (plus m p) in (lt n0 TMP_2))) in (let TMP_4 \def (plus p 
-n) in (let TMP_5 \def (plus_sym n p) in (let H0 \def (eq_ind nat TMP_1 TMP_3 
-H TMP_4 TMP_5) in (let TMP_6 \def (plus m p) in (let TMP_8 \def (\lambda (n0: 
-nat).(let TMP_7 \def (plus p n) in (lt TMP_7 n0))) in (let TMP_9 \def (plus p 
-m) in (let TMP_10 \def (plus_sym m p) in (let H1 \def (eq_ind nat TMP_6 TMP_8 
-H0 TMP_9 TMP_10) in (simpl_lt_plus_l n m p H1)))))))))))))).
-
-theorem minus_x_Sy:
+n p) (plus m p))).(simpl_lt_plus_l n m p (let H0 \def (eq_ind nat (plus n p) 
+(\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_sym n p)) in (let 
+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)))))).
+
+lemma minus_x_Sy:

  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S 
 (minus x (S y))))))
 \def
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S 
 (minus x (S y))))))
 \def

- \lambda (x: nat).(let TMP_5 \def (\lambda (n: nat).(\forall (y: nat).((lt y 
-n) \to (let TMP_1 \def (minus n y) in (let TMP_2 \def (S y) in (let TMP_3 
-\def (minus n TMP_2) in (let TMP_4 \def (S TMP_3) in (eq nat TMP_1 
-TMP_4)))))))) in (let TMP_22 \def (\lambda (y: nat).(\lambda (H: (lt y 
-O)).(let H0 \def (match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) 
-O)).(let TMP_14 \def (S y) in (let TMP_15 \def (\lambda (e: nat).(match e 
-with [O \Rightarrow False | (S _) \Rightarrow True])) in (let H1 \def (eq_ind 
-nat TMP_14 TMP_15 I O H0) in (let TMP_16 \def (minus O y) in (let TMP_17 \def 
-(S y) in (let TMP_18 \def (minus O TMP_17) in (let TMP_19 \def (S TMP_18) in 
-(let TMP_20 \def (eq nat TMP_16 TMP_19) in (False_ind TMP_20 H1)))))))))) | 
-(le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).(let TMP_6 \def (S m) 
-in (let TMP_7 \def (\lambda (e: nat).(match e with [O \Rightarrow False | (S 
-_) \Rightarrow True])) in (let H2 \def (eq_ind nat TMP_6 TMP_7 I O H1) in 
-(let TMP_12 \def ((le (S y) m) \to (let TMP_8 \def (minus O y) in (let TMP_9 
-\def (S y) in (let TMP_10 \def (minus O TMP_9) in (let TMP_11 \def (S TMP_10) 
-in (eq nat TMP_8 TMP_11)))))) in (let TMP_13 \def (False_ind TMP_12 H2) in 
-(TMP_13 H0)))))))]) in (let TMP_21 \def (refl_equal nat O) in (H0 TMP_21))))) 
-in (let TMP_40 \def (\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).(let 
-TMP_29 \def (\lambda (n0: nat).((lt n0 (S n)) \to (let TMP_23 \def (S n) in 
-(let TMP_24 \def (minus TMP_23 n0) in (let TMP_25 \def (S n) in (let TMP_26 
-\def (S n0) in (let TMP_27 \def (minus TMP_25 TMP_26) in (let TMP_28 \def (S 
-TMP_27) in (eq nat TMP_24 TMP_28))))))))) in (let TMP_37 \def (\lambda (_: 
-(lt O (S n))).(let TMP_32 \def (\lambda (n0: nat).(let TMP_30 \def (S n) in 
-(let TMP_31 \def (S n0) in (eq nat TMP_30 TMP_31)))) in (let TMP_33 \def (S 
-n) in (let TMP_34 \def (refl_equal nat TMP_33) in (let TMP_35 \def (minus n 
-O) in (let TMP_36 \def (minus_n_O n) in (eq_ind nat n TMP_32 TMP_34 TMP_35 
-TMP_36))))))) in (let TMP_39 \def (\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 TMP_38 \def (S n0) in (let H2 \def (le_S_n TMP_38 n 
-H1) in (H n0 H2)))))) in (nat_ind TMP_29 TMP_37 TMP_39 y))))))) in (nat_ind 
-TMP_5 TMP_22 TMP_40 x)))).
-
-theorem lt_plus_minus:
+ \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 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).
+
+lemma lt_plus_minus:

  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus 
 y (S x)))))))
 \def
  \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)).(let TMP_1 \def (S 
-x) in (le_plus_minus TMP_1 y H)))).
+ \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S 
+x) y H))).

 
 

-theorem lt_plus_minus_r:
+lemma lt_plus_minus_r:

  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y 
 (S x)) x)))))
 \def
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y 
 (S x)) x)))))
 \def

- \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(let TMP_1 \def (S 
-x) in (let TMP_2 \def (minus y TMP_1) in (let TMP_3 \def (plus x TMP_2) in 
-(let TMP_5 \def (\lambda (n: nat).(let TMP_4 \def (S n) in (eq nat y TMP_4))) 
-in (let TMP_6 \def (lt_plus_minus x y H) in (let TMP_7 \def (S x) in (let 
-TMP_8 \def (minus y TMP_7) in (let TMP_9 \def (plus TMP_8 x) in (let TMP_10 
-\def (S x) in (let TMP_11 \def (minus y TMP_10) in (let TMP_12 \def (plus_sym 
-TMP_11 x) in (eq_ind_r nat TMP_3 TMP_5 TMP_6 TMP_9 TMP_12)))))))))))))).
+ \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat 
+(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)))).

 
 

-theorem minus_x_SO:
+lemma minus_x_SO:

  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
 \def
  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
 \def

- \lambda (x: nat).(\lambda (H: (lt O x)).(let TMP_1 \def (minus x O) in (let 
-TMP_2 \def (\lambda (n: nat).(eq nat x n)) in (let TMP_3 \def (\lambda (n: 
-nat).(eq nat x n)) in (let TMP_4 \def (refl_equal nat x) in (let TMP_5 \def 
-(minus x O) in (let TMP_6 \def (minus_n_O x) in (let TMP_7 \def (eq_ind nat x 
-TMP_3 TMP_4 TMP_5 TMP_6) in (let TMP_8 \def (S O) in (let TMP_9 \def (minus x 
-TMP_8) in (let TMP_10 \def (S TMP_9) in (let TMP_11 \def (minus_x_Sy x O H) 
-in (eq_ind nat TMP_1 TMP_2 TMP_7 TMP_10 TMP_11))))))))))))).
+ \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))).

 
 

-theorem le_x_pred_y:
+lemma le_x_pred_y:

  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
 \def
  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
 \def

- \lambda (y: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (x: nat).((lt x 
-n) \to (let TMP_1 \def (pred n) in (le x TMP_1))))) in (let TMP_11 \def 
-(\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def (match H with [le_n 
-\Rightarrow (\lambda (H0: (eq nat (S x) O)).(let TMP_7 \def (S x) in (let 
-TMP_8 \def (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) 
-\Rightarrow True])) in (let H1 \def (eq_ind nat TMP_7 TMP_8 I O H0) in (let 
-TMP_9 \def (le x O) in (False_ind TMP_9 H1)))))) | (le_S m H0) \Rightarrow 
-(\lambda (H1: (eq nat (S m) O)).(let TMP_3 \def (S m) in (let TMP_4 \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 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 
 (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow 

-True])) in (let H2 \def (eq_ind nat TMP_3 TMP_4 I O H1) in (let TMP_5 \def 
-((le (S x) m) \to (le x O)) in (let TMP_6 \def (False_ind TMP_5 H2) in (TMP_6 
-H0)))))))]) in (let TMP_10 \def (refl_equal nat O) in (H0 TMP_10))))) in (let 
-TMP_12 \def (\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))))) in (nat_ind TMP_2 TMP_11 TMP_12 y)))).
-
-theorem lt_le_minus:
+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).
+
+lemma lt_le_minus:

  \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
 \def
  \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)).(let TMP_1 \def (S 
-O) in (let TMP_2 \def (S O) in (let TMP_3 \def (plus TMP_2 x) in (let TMP_4 
-\def (\lambda (n: nat).(le n y)) in (let TMP_5 \def (S O) in (let TMP_6 \def 
-(plus x TMP_5) in (let TMP_7 \def (S O) in (let TMP_8 \def (plus_sym x TMP_7) 
-in (let TMP_9 \def (eq_ind_r nat TMP_3 TMP_4 H TMP_6 TMP_8) in (le_minus x y 
-TMP_1 TMP_9)))))))))))).
+ \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)))))).

 
 

-theorem lt_le_e:
+lemma lt_le_e:

  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) 
 \to ((((le d n) \to P)) \to P))))
 \def
  \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n 
 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in 
  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) 
 \to ((((le d n) \to P)) \to P))))
 \def
  \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n 
 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in 

-(let TMP_1 \def (le d n) in (let TMP_2 \def (lt n d) in (or_ind TMP_1 TMP_2 P 
-H0 H H1)))))))).
+(or_ind (le d n) (lt n d) P H0 H H1)))))).

 
 

-theorem lt_eq_e:
+lemma lt_eq_e:

  \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
  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x 
  \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
  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x 

-y)).(let TMP_1 \def (lt x y) in (let TMP_2 \def (eq nat x y) in (let TMP_3 
-\def (le_lt_or_eq x y H1) in (or_ind TMP_1 TMP_2 P H H0 TMP_3))))))))).
+y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).

 
 

-theorem lt_eq_gt_e:
+lemma lt_eq_gt_e:

  \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
  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x) 
  \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
  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x) 

-\to P))).(let TMP_3 \def (\lambda (H2: (le y x)).(let TMP_2 \def (\lambda 
-(H3: (eq nat y x)).(let TMP_1 \def (sym_eq nat y x H3) in (H0 TMP_1))) in 
-(lt_eq_e y x P H1 TMP_2 H2))) in (lt_le_e x y P H TMP_3))))))).
+\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)))))))).

 
 

-theorem lt_gen_xS:
+lemma lt_gen_xS:

  \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

- \lambda (x: nat).(let TMP_6 \def (\lambda (n: nat).(\forall (n0: nat).((lt n 
-(S n0)) \to (let TMP_1 \def (eq nat n O) in (let TMP_3 \def (\lambda (m: 
-nat).(let TMP_2 \def (S m) in (eq nat n TMP_2))) in (let TMP_4 \def (\lambda 
-(m: nat).(lt m n0)) in (let TMP_5 \def (ex2 nat TMP_3 TMP_4) in (or TMP_1 
-TMP_5)))))))) in (let TMP_13 \def (\lambda (n: nat).(\lambda (_: (lt O (S 
-n))).(let TMP_7 \def (eq nat O O) in (let TMP_9 \def (\lambda (m: nat).(let 
-TMP_8 \def (S m) in (eq nat O TMP_8))) in (let TMP_10 \def (\lambda (m: 
-nat).(lt m n)) in (let TMP_11 \def (ex2 nat TMP_9 TMP_10) in (let TMP_12 \def 
-(refl_equal nat O) in (or_introl TMP_7 TMP_11 TMP_12)))))))) in (let TMP_30 
-\def (\lambda (n: nat).(\lambda (_: ((\forall (n0: nat).((lt n (S n0)) \to 
-(or (eq nat n O) (ex2 nat (\lambda (m: nat).(eq nat n (S m))) (\lambda (m: 
-nat).(lt m n0)))))))).(\lambda (n0: nat).(\lambda (H0: (lt (S n) (S 
-n0))).(let TMP_14 \def (S n) in (let TMP_15 \def (eq nat TMP_14 O) in (let 
-TMP_18 \def (\lambda (m: nat).(let TMP_16 \def (S n) in (let TMP_17 \def (S 
-m) in (eq nat TMP_16 TMP_17)))) in (let TMP_19 \def (\lambda (m: nat).(lt m 
-n0)) in (let TMP_20 \def (ex2 nat TMP_18 TMP_19) in (let TMP_23 \def (\lambda 
-(m: nat).(let TMP_21 \def (S n) in (let TMP_22 \def (S m) in (eq nat TMP_21 
-TMP_22)))) in (let TMP_24 \def (\lambda (m: nat).(lt m n0)) in (let TMP_25 
-\def (S n) in (let TMP_26 \def (refl_equal nat TMP_25) in (let TMP_27 \def (S 
-n) in (let TMP_28 \def (le_S_n TMP_27 n0 H0) in (let TMP_29 \def (ex_intro2 
-nat TMP_23 TMP_24 n TMP_26 TMP_28) in (or_intror TMP_15 TMP_20 
-TMP_29))))))))))))))))) in (nat_ind TMP_6 TMP_13 TMP_30 x)))).
-
-theorem le_lt_false:
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).((lt n (S 
+n0)) \to (or (eq nat n O) (ex2 nat (\lambda (m: nat).(eq nat n (S m))) 
+(\lambda (m: nat).(lt m n0))))))) (\lambda (n: nat).(\lambda (_: (lt O (S 
+n))).(or_introl (eq nat O O) (ex2 nat (\lambda (m: nat).(eq nat O (S m))) 
+(\lambda (m: nat).(lt m n))) (refl_equal nat O)))) (\lambda (n: nat).(\lambda 
+(_: ((\forall (n0: nat).((lt n (S n0)) \to (or (eq nat n O) (ex2 nat (\lambda 
+(m: nat).(eq nat n (S m))) (\lambda (m: nat).(lt m n0)))))))).(\lambda (n0: 
+nat).(\lambda (H0: (lt (S n) (S n0))).(or_intror (eq nat (S n) O) (ex2 nat 
+(\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0))) 
+(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).
+
+lemma le_lt_false:

  \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 
  \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).(let TMP_1 \def (le_not_lt x y H H0) in (False_ind P 
-TMP_1)))))).
+y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).

 
 

-theorem lt_neq:
+lemma lt_neq:

  \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 
  \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 TMP_1 \def (\lambda (n: nat).(lt n y)) in (let H1 \def (eq_ind 
-nat x TMP_1 H y H0) in (lt_n_n y H1)))))).
+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))))).

 
 

-theorem arith0:
+lemma arith0:

  \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
  \lambda (h2: nat).(\lambda (d2: nat).(\lambda (n: nat).(\lambda (H: (le 
  \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
  \lambda (h2: nat).(\lambda (d2: nat).(\lambda (n: nat).(\lambda (H: (le 

-(plus d2 h2) n)).(\lambda (h1: nat).(let TMP_1 \def (plus d2 h1) in (let 
-TMP_2 \def (plus h2 TMP_1) in (let TMP_3 \def (minus TMP_2 h2) in (let TMP_6 
-\def (\lambda (n0: nat).(let TMP_4 \def (plus n h1) in (let TMP_5 \def (minus 
-TMP_4 h2) in (le n0 TMP_5)))) in (let TMP_7 \def (plus d2 h1) in (let TMP_8 
-\def (plus h2 TMP_7) in (let TMP_9 \def (plus d2 h1) in (let TMP_10 \def 
-(le_plus_l h2 TMP_9) in (let TMP_11 \def (plus n h1) in (let TMP_12 \def 
-(plus h2 d2) in (let TMP_13 \def (plus TMP_12 h1) in (let TMP_15 \def 
-(\lambda (n0: nat).(let TMP_14 \def (plus n h1) in (le n0 TMP_14))) in (let 
-TMP_16 \def (plus d2 h2) in (let TMP_19 \def (\lambda (n0: nat).(let TMP_17 
-\def (plus n0 h1) in (let TMP_18 \def (plus n h1) in (le TMP_17 TMP_18)))) in 
-(let TMP_20 \def (plus d2 h2) in (let TMP_21 \def (plus TMP_20 h1) in (let 
-TMP_22 \def (plus n h1) in (let TMP_23 \def (plus d2 h2) in (let TMP_24 \def 
-(plus TMP_23 h1) in (let TMP_25 \def (plus n h1) in (let TMP_26 \def (plus d2 
-h2) in (let TMP_27 \def (le_n h1) in (let TMP_28 \def (le_plus_plus TMP_26 n 
-h1 h1 H TMP_27) in (let TMP_29 \def (le_n_S TMP_24 TMP_25 TMP_28) in (let 
-TMP_30 \def (le_S_n TMP_21 TMP_22 TMP_29) in (let TMP_31 \def (plus h2 d2) in 
-(let TMP_32 \def (plus_sym h2 d2) in (let TMP_33 \def (eq_ind_r nat TMP_16 
-TMP_19 TMP_30 TMP_31 TMP_32) in (let TMP_34 \def (plus d2 h1) in (let TMP_35 
-\def (plus h2 TMP_34) in (let TMP_36 \def (plus_assoc_l h2 d2 h1) in (let 
-TMP_37 \def (eq_ind_r nat TMP_13 TMP_15 TMP_33 TMP_35 TMP_36) in (let TMP_38 
-\def (le_minus_minus h2 TMP_8 TMP_10 TMP_11 TMP_37) in (let TMP_39 \def (plus 
-d2 h1) in (let TMP_40 \def (plus d2 h1) in (let TMP_41 \def (minus_plus h2 
-TMP_40) in (eq_ind nat TMP_3 TMP_6 TMP_38 TMP_39 
-TMP_41))))))))))))))))))))))))))))))))))))))))).
-
-theorem O_minus:
+(plus d2 h2) n)).(\lambda (h1: nat).(eq_ind nat (minus (plus h2 (plus d2 h1)) 
+h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2 
+(plus h2 (plus d2 h1)) (le_plus_l h2 (plus d2 h1)) (plus n h1) (eq_ind_r nat 
+(plus (plus h2 d2) h1) (\lambda (n0: nat).(le n0 (plus n h1))) (eq_ind_r nat 
+(plus d2 h2) (\lambda (n0: nat).(le (plus n0 h1) (plus n h1))) (le_S_n (plus 
+(plus d2 h2) h1) (plus n h1) (le_n_S (plus (plus d2 h2) h1) (plus n h1) 
+(le_plus_plus (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_sym h2 
+d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1) 
+(minus_plus h2 (plus d2 h1))))))).
+
+lemma O_minus:

  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
 \def
  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
 \def

- \lambda (x: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (y: nat).((le n 
-y) \to (let TMP_1 \def (minus n y) in (eq nat TMP_1 O))))) in (let TMP_3 \def 
-(\lambda (y: nat).(\lambda (_: (le O y)).(refl_equal nat O))) in (let TMP_20 
-\def (\lambda (x0: nat).(\lambda (H: ((\forall (y: nat).((le x0 y) \to (eq 
-nat (minus x0 y) O))))).(\lambda (y: nat).(let TMP_5 \def (\lambda (n: 
-nat).((le (S x0) n) \to (let TMP_4 \def (match n with [O \Rightarrow (S x0) | 
-(S l) \Rightarrow (minus x0 l)]) in (eq nat TMP_4 O)))) in (let TMP_17 \def 
-(\lambda (H0: (le (S x0) O)).(let TMP_7 \def (\lambda (n: nat).(let TMP_6 
-\def (S n) in (eq nat O TMP_6))) in (let TMP_8 \def (\lambda (n: nat).(le x0 
-n)) in (let TMP_9 \def (S x0) in (let TMP_10 \def (eq nat TMP_9 O) in (let 
-TMP_15 \def (\lambda (x1: nat).(\lambda (H1: (eq nat O (S x1))).(\lambda (_: 
-(le x0 x1)).(let TMP_11 \def (\lambda (ee: nat).(match ee with [O \Rightarrow 
-True | (S _) \Rightarrow False])) in (let TMP_12 \def (S x1) in (let H3 \def 
-(eq_ind nat O TMP_11 I TMP_12 H1) in (let TMP_13 \def (S x0) in (let TMP_14 
-\def (eq nat TMP_13 O) in (False_ind TMP_14 H3))))))))) in (let TMP_16 \def 
-(le_gen_S x0 O H0) in (ex2_ind nat TMP_7 TMP_8 TMP_10 TMP_15 TMP_16)))))))) 
-in (let TMP_19 \def (\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))).(let TMP_18 \def (le_S_n x0 n H1) in 
-(H n TMP_18))))) in (nat_ind TMP_5 TMP_17 TMP_19 y))))))) in (nat_ind TMP_2 
-TMP_3 TMP_20 x)))).
-
-theorem minus_minus:
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to 
+(eq nat (minus n y) O)))) (\lambda (y: nat).(\lambda (_: (le O 
+y)).(refl_equal nat O))) (\lambda (x0: nat).(\lambda (H: ((\forall (y: 
+nat).((le x0 y) \to (eq nat (minus x0 y) O))))).(\lambda (y: nat).(nat_ind 
+(\lambda (n: nat).((le (S x0) n) \to (eq nat (match n with [O \Rightarrow (S 
+x0) | (S l) \Rightarrow (minus x0 l)]) O))) (\lambda (H0: (le (S x0) 
+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 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).
+
+lemma minus_minus:

  \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

- \lambda (z: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (x: 
-nat).(\forall (y: nat).((le n x) \to ((le n y) \to ((eq nat (minus x n) 
-(minus y n)) \to (eq nat x y))))))) in (let TMP_9 \def (\lambda (x: 
-nat).(\lambda (y: nat).(\lambda (_: (le O x)).(\lambda (_: (le O y)).(\lambda 
-(H1: (eq nat (minus x O) (minus y O))).(let TMP_2 \def (minus x O) in (let 
-TMP_4 \def (\lambda (n: nat).(let TMP_3 \def (minus y O) in (eq nat n 
-TMP_3))) in (let TMP_5 \def (minus_n_O x) in (let H2 \def (eq_ind_r nat TMP_2 
-TMP_4 H1 x TMP_5) in (let TMP_6 \def (minus y O) in (let TMP_7 \def (\lambda 
-(n: nat).(eq nat x n)) in (let TMP_8 \def (minus_n_O y) in (let H3 \def 
-(eq_ind_r nat TMP_6 TMP_7 H2 y TMP_8) in H3))))))))))))) in (let TMP_40 \def 
-(\lambda (z0: nat).(\lambda (IH: ((\forall (x: nat).(\forall (y: nat).((le z0 
-x) \to ((le z0 y) \to ((eq nat (minus x z0) (minus y z0)) \to (eq nat x 
-y)))))))).(\lambda (x: nat).(let TMP_10 \def (\lambda (n: nat).(\forall (y: 
-nat).((le (S z0) n) \to ((le (S z0) y) \to ((eq nat (minus n (S z0)) (minus y 
-(S z0))) \to (eq nat n y)))))) in (let TMP_20 \def (\lambda (y: nat).(\lambda 
-(H: (le (S z0) O)).(\lambda (_: (le (S z0) y)).(\lambda (_: (eq nat (minus O 
-(S z0)) (minus y (S z0)))).(let TMP_12 \def (\lambda (n: nat).(let TMP_11 
-\def (S n) in (eq nat O TMP_11))) in (let TMP_13 \def (\lambda (n: nat).(le 
-z0 n)) in (let TMP_14 \def (eq nat O y) in (let TMP_18 \def (\lambda (x0: 
-nat).(\lambda (H2: (eq nat O (S x0))).(\lambda (_: (le z0 x0)).(let TMP_15 
-\def (\lambda (ee: nat).(match ee with [O \Rightarrow True | (S _) 
-\Rightarrow False])) in (let TMP_16 \def (S x0) in (let H4 \def (eq_ind nat O 
-TMP_15 I TMP_16 H2) in (let TMP_17 \def (eq nat O y) in (False_ind TMP_17 
-H4)))))))) in (let TMP_19 \def (le_gen_S z0 O H) in (ex2_ind nat TMP_12 
-TMP_13 TMP_14 TMP_18 TMP_19)))))))))) in (let TMP_39 \def (\lambda (x0: 
+ \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).(\forall (y: 
+nat).((le n x) \to ((le n y) \to ((eq nat (minus x n) (minus y n)) \to (eq 
+nat x y))))))) (\lambda (x: nat).(\lambda (y: nat).(\lambda (_: (le O 
+x)).(\lambda (_: (le O y)).(\lambda (H1: (eq nat (minus x O) (minus y 
+O))).(let H2 \def (eq_ind_r nat (minus x O) (\lambda (n: nat).(eq nat n 
+(minus y O))) H1 x (minus_n_O x)) in (let H3 \def (eq_ind_r nat (minus y O) 
+(\lambda (n: nat).(eq nat x n)) H2 y (minus_n_O y)) in H3))))))) (\lambda 
+(z0: nat).(\lambda (IH: ((\forall (x: nat).(\forall (y: nat).((le z0 x) \to 
+((le z0 y) \to ((eq nat (minus x z0) (minus y z0)) \to (eq nat x 
+y)))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le 
+(S z0) n) \to ((le (S z0) y) \to ((eq nat (minus n (S z0)) (minus y (S z0))) 
+\to (eq nat n y)))))) (\lambda (y: nat).(\lambda (H: (le (S z0) O)).(\lambda 
+(_: (le (S z0) y)).(\lambda (_: (eq nat (minus O (S z0)) (minus y (S 
+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 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 
 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).(let TMP_22 \def (\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 (let TMP_21 
-\def (S x0) in (eq nat TMP_21 n)))))) in (let TMP_34 \def (\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 (let TMP_24 \def 
-(\lambda (n: nat).(let TMP_23 \def (S n) in (eq nat O TMP_23))) in (let 
-TMP_25 \def (\lambda (n: nat).(le z0 n)) in (let TMP_26 \def (S x0) in (let 
-TMP_27 \def (eq nat TMP_26 O) in (let TMP_32 \def (\lambda (x1: nat).(\lambda 
-(H2: (eq nat O (S x1))).(\lambda (_: (le z0 x1)).(let TMP_28 \def (\lambda 
-(ee: nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) in 
-(let TMP_29 \def (S x1) in (let H4 \def (eq_ind nat O TMP_28 I TMP_29 H2) in 
-(let TMP_30 \def (S x0) in (let TMP_31 \def (eq nat TMP_30 O) in (False_ind 
-TMP_31 H4))))))))) in (let TMP_33 \def (le_gen_S z0 O H0) in (ex2_ind nat 
-TMP_24 TMP_25 TMP_27 TMP_32 TMP_33))))))))))) in (let TMP_38 \def (\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 
 (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)))).(let TMP_35 \def (le_S_n z0 
-x0 H) in (let TMP_36 \def (le_S_n z0 y0 H0) in (let TMP_37 \def (IH x0 y0 
-TMP_35 TMP_36 H1) in (f_equal nat nat S x0 y0 TMP_37))))))))) in (nat_ind 
-TMP_22 TMP_34 TMP_38 y))))))) in (nat_ind TMP_10 TMP_20 TMP_39 x))))))) in 
-(nat_ind TMP_1 TMP_9 TMP_40 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).

 
 

-theorem plus_plus:
+lemma plus_plus:

  \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)))))))))
 \def
  \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)))))))))
 \def

- \lambda (z: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (x1: 
-nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 n) \to 
-((le x2 n) \to ((eq nat (plus (minus n x1) y1) (plus (minus n x2) y2)) \to 
-(let TMP_1 \def (plus x1 y2) in (let TMP_2 \def (plus x2 y1) in (eq nat TMP_1 
-TMP_2))))))))))) in (let TMP_17 \def (\lambda (x1: nat).(\lambda (x2: 
-nat).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le x1 O)).(\lambda 
-(H0: (le x2 O)).(\lambda (H1: (eq nat y1 y2)).(let TMP_6 \def (\lambda (n: 
-nat).(let TMP_4 \def (plus x1 n) in (let TMP_5 \def (plus x2 y1) in (eq nat 
-TMP_4 TMP_5)))) in (let H_y \def (le_n_O_eq x2 H0) in (let TMP_9 \def 
-(\lambda (n: nat).(let TMP_7 \def (plus x1 y1) in (let TMP_8 \def (plus n y1) 
-in (eq nat TMP_7 TMP_8)))) in (let H_y0 \def (le_n_O_eq x1 H) in (let TMP_12 
-\def (\lambda (n: nat).(let TMP_10 \def (plus n y1) in (let TMP_11 \def (plus 
-O y1) in (eq nat TMP_10 TMP_11)))) in (let TMP_13 \def (plus O y1) in (let 
-TMP_14 \def (refl_equal nat TMP_13) in (let TMP_15 \def (eq_ind nat O TMP_12 
-TMP_14 x1 H_y0) in (let TMP_16 \def (eq_ind nat O TMP_9 TMP_15 x2 H_y) in 
-(eq_ind nat y1 TMP_6 TMP_16 y2 H1))))))))))))))))) in (let TMP_91 \def 
+ \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x1: nat).(\forall (x2: 
+nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 n) \to ((le x2 n) \to ((eq 
+nat (plus (minus n x1) y1) (plus (minus n x2) y2)) \to (eq nat (plus x1 y2) 
+(plus x2 y1)))))))))) (\lambda (x1: nat).(\lambda (x2: nat).(\lambda (y1: 
+nat).(\lambda (y2: nat).(\lambda (H: (le x1 O)).(\lambda (H0: (le x2 
+O)).(\lambda (H1: (eq nat y1 y2)).(eq_ind nat y1 (\lambda (n: nat).(eq nat 
+(plus x1 n) (plus x2 y1))) (let H_y \def (le_n_O_eq x2 H0) in (eq_ind nat O 
+(\lambda (n: nat).(eq nat (plus x1 y1) (plus n y1))) (let H_y0 \def 
+(le_n_O_eq x1 H) in (eq_ind nat O (\lambda (n: nat).(eq nat (plus n y1) (plus 
+O y1))) (refl_equal nat (plus O y1)) x1 H_y0)) x2 H_y)) y2 H1)))))))) 

 (\lambda (z0: nat).(\lambda (IH: ((\forall (x1: nat).(\forall (x2: 
 nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z0) \to ((le x2 z0) \to 
 ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2)) \to (eq nat (plus 
 (\lambda (z0: nat).(\lambda (IH: ((\forall (x1: nat).(\forall (x2: 
 nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z0) \to ((le x2 z0) \to 
 ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2)) \to (eq nat (plus 

-x1 y2) (plus x2 y1))))))))))).(\lambda (x1: nat).(let TMP_20 \def (\lambda 
-(n: nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le n (S 
-z0)) \to ((le x2 (S z0)) \to ((eq nat (plus (minus (S z0) n) y1) (plus (minus 
-(S z0) x2) y2)) \to (let TMP_18 \def (plus n y2) in (let TMP_19 \def (plus x2 
-y1) in (eq nat TMP_18 TMP_19)))))))))) in (let TMP_56 \def (\lambda (x2: 
-nat).(let TMP_23 \def (\lambda (n: nat).(\forall (y1: nat).(\forall (y2: 
-nat).((le O (S z0)) \to ((le n (S z0)) \to ((eq nat (plus (minus (S z0) O) 
-y1) (plus (minus (S z0) n) y2)) \to (let TMP_21 \def (plus O y2) in (let 
-TMP_22 \def (plus n y1) in (eq nat TMP_21 TMP_22))))))))) in (let TMP_32 \def 
-(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda 
-(_: (le O (S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (S (plus z0 
-y2)))).(let H_y \def (IH O O) in (let TMP_24 \def (minus z0 O) in (let TMP_25 
-\def (\lambda (n: nat).(\forall (y3: nat).(\forall (y4: nat).((le O z0) \to 
-((le O z0) \to ((eq nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) in 
-(let TMP_26 \def (minus_n_O z0) in (let H2 \def (eq_ind_r nat TMP_24 TMP_25 
-H_y z0 TMP_26) in (let TMP_27 \def (le_O_n z0) in (let TMP_28 \def (le_O_n 
-z0) in (let TMP_29 \def (plus z0 y1) in (let TMP_30 \def (plus z0 y2) in (let 
-TMP_31 \def (eq_add_S TMP_29 TMP_30 H1) in (H2 y1 y2 TMP_27 TMP_28 
-TMP_31)))))))))))))))) in (let TMP_55 \def (\lambda (x3: nat).(\lambda (_: 
-((\forall (y1: nat).(\forall (y2: nat).((le O (S z0)) \to ((le x3 (S z0)) \to 
-((eq nat (S (plus z0 y1)) (plus (match x3 with [O \Rightarrow (S z0) | (S l) 
-\Rightarrow (minus z0 l)]) y2)) \to (eq nat y2 (plus x3 y1))))))))).(\lambda 
-(y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S 
-x3) (S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) 
-y2))).(let TMP_33 \def (S y1) in (let H_y \def (IH O x3 TMP_33) in (let 
-TMP_34 \def (minus z0 O) in (let TMP_37 \def (\lambda (n: nat).(\forall (y3: 
-nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S y1)) (plus (minus z0 
-x3) y3)) \to (let TMP_35 \def (S y1) in (let TMP_36 \def (plus x3 TMP_35) in 
-(eq nat y3 TMP_36)))))))) in (let TMP_38 \def (minus_n_O z0) in (let H2 \def 
-(eq_ind_r nat TMP_34 TMP_37 H_y z0 TMP_38) in (let TMP_39 \def (S y1) in (let 
-TMP_40 \def (plus z0 TMP_39) in (let TMP_43 \def (\lambda (n: nat).(\forall 
-(y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus (minus z0 x3) y3)) 
-\to (let TMP_41 \def (S y1) in (let TMP_42 \def (plus x3 TMP_41) in (eq nat 
-y3 TMP_42)))))))) in (let TMP_44 \def (plus z0 y1) in (let TMP_45 \def (S 
-TMP_44) in (let TMP_46 \def (plus_n_Sm z0 y1) in (let H3 \def (eq_ind_r nat 
-TMP_40 TMP_43 H2 TMP_45 TMP_46) in (let TMP_47 \def (S y1) in (let TMP_48 
-\def (plus x3 TMP_47) in (let TMP_49 \def (\lambda (n: nat).(\forall (y3: 
-nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus z0 y1)) (plus (minus z0 
-x3) y3)) \to (eq nat y3 n)))))) in (let TMP_50 \def (plus x3 y1) in (let 
-TMP_51 \def (S TMP_50) in (let TMP_52 \def (plus_n_Sm x3 y1) in (let H4 \def 
-(eq_ind_r nat TMP_48 TMP_49 H3 TMP_51 TMP_52) in (let TMP_53 \def (le_O_n z0) 
-in (let TMP_54 \def (le_S_n x3 z0 H0) in (H4 y2 TMP_53 TMP_54 
-H1)))))))))))))))))))))))))))))) in (nat_ind TMP_23 TMP_32 TMP_55 x2))))) in 
-(let TMP_90 \def (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall 
-(y1: nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat 
+x1 y2) (plus x2 y1))))))))))).(\lambda (x1: nat).(nat_ind (\lambda (n: 
+nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le n (S z0)) 
+\to ((le x2 (S z0)) \to ((eq nat (plus (minus (S z0) n) y1) (plus (minus (S 
+z0) x2) y2)) \to (eq nat (plus n y2) (plus x2 y1))))))))) (\lambda (x2: 
+nat).(nat_ind (\lambda (n: nat).(\forall (y1: nat).(\forall (y2: nat).((le O 
+(S z0)) \to ((le n (S z0)) \to ((eq nat (plus (minus (S z0) O) y1) (plus 
+(minus (S z0) n) y2)) \to (eq nat (plus O y2) (plus n y1)))))))) (\lambda 
+(y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda (_: (le O 
+(S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (S (plus z0 y2)))).(let H_y 
+\def (IH O O) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n: 
+nat).(\forall (y3: nat).(\forall (y4: nat).((le O z0) \to ((le O z0) \to ((eq 
+nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) H_y z0 (minus_n_O z0)) 
+in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (eq_add_S (plus z0 y1) (plus z0 y2) 
+H1))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2: 
+nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) (plus 
+(match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2)) 
+\to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2: 
+nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S x3) (S z0))).(\lambda 
+(H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2))).(let H_y \def (IH O 
+x3 (S y1)) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n: 
+nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S 
+y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H_y z0 
+(minus_n_O z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda (n: 
+nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus 
+(minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1)) 
+(plus_n_Sm z0 y1)) in (let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda 
+(n: nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus 
+z0 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 n)))))) H3 (S (plus x3 y1)) 
+(plus_n_Sm x3 y1)) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1)))))))))))) 
+x2)) (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall (y1: 
+nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat 

 (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2 
 (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2 

-y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(let TMP_60 \def (\lambda (n: 
+y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(nat_ind (\lambda (n: 

 nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S 
 z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2)) 
 nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S 
 z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2)) 

-\to (let TMP_57 \def (S x2) in (let TMP_58 \def (plus TMP_57 y2) in (let 
-TMP_59 \def (plus n y1) in (eq nat TMP_58 TMP_59)))))))))) in (let TMP_83 
-\def (\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S 
-z0))).(\lambda (_: (le O (S z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) 
-y1) (S (plus z0 y2)))).(let TMP_61 \def (S y2) in (let H_y \def (IH x2 O y1 
-TMP_61) in (let TMP_62 \def (minus z0 O) in (let TMP_65 \def (\lambda (n: 
-nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) (plus n 
-(S y2))) \to (let TMP_63 \def (S y2) in (let TMP_64 \def (plus x2 TMP_63) in 
-(eq nat TMP_64 y1))))))) in (let TMP_66 \def (minus_n_O z0) in (let H2 \def 
-(eq_ind_r nat TMP_62 TMP_65 H_y z0 TMP_66) in (let TMP_67 \def (S y2) in (let 
-TMP_68 \def (plus z0 TMP_67) in (let TMP_71 \def (\lambda (n: nat).((le x2 
-z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (let TMP_69 
-\def (S y2) in (let TMP_70 \def (plus x2 TMP_69) in (eq nat TMP_70 y1))))))) 
-in (let TMP_72 \def (plus z0 y2) in (let TMP_73 \def (S TMP_72) in (let 
-TMP_74 \def (plus_n_Sm z0 y2) in (let H3 \def (eq_ind_r nat TMP_68 TMP_71 H2 
-TMP_73 TMP_74) in (let TMP_75 \def (S y2) in (let TMP_76 \def (plus x2 
-TMP_75) in (let TMP_77 \def (\lambda (n: nat).((le x2 z0) \to ((le O z0) \to 
-((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1))))) in 
-(let TMP_78 \def (plus x2 y2) in (let TMP_79 \def (S TMP_78) in (let TMP_80 
-\def (plus_n_Sm x2 y2) in (let H4 \def (eq_ind_r nat TMP_76 TMP_77 H3 TMP_79 
-TMP_80) in (let TMP_81 \def (le_S_n x2 z0 H) in (let TMP_82 \def (le_O_n z0) 
-in (H4 TMP_81 TMP_82 H1)))))))))))))))))))))))))))) in (let TMP_89 \def 
-(\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2: nat).((le 
-(S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus z0 x2) y1) (plus 
-(match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2)) 
-\to (eq nat (S (plus x2 y2)) (plus x4 y1))))))))).(\lambda (y1: nat).(\lambda 
-(y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (H0: (le (S x4) (S 
-z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4) 
-y2))).(let TMP_84 \def (plus x2 y2) in (let TMP_85 \def (plus x4 y1) in (let 
-TMP_86 \def (le_S_n x2 z0 H) in (let TMP_87 \def (le_S_n x4 z0 H0) in (let 
-TMP_88 \def (IH x2 x4 y1 y2 TMP_86 TMP_87 H1) in (f_equal nat nat S TMP_84 
-TMP_85 TMP_88))))))))))))) in (nat_ind TMP_60 TMP_83 TMP_89 x3))))))) in 
-(nat_ind TMP_20 TMP_56 TMP_90 x1))))))) in (nat_ind TMP_3 TMP_17 TMP_91 z)))).
-
-theorem le_S_minus:
+\to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda (y1: nat).(\lambda 
+(y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (_: (le O (S 
+z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))).(let 
+H_y \def (IH x2 O y1 (S y2)) in (let H2 \def (eq_ind_r nat (minus z0 O) 
+(\lambda (n: nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) 
+y1) (plus n (S y2))) \to (eq nat (plus x2 (S y2)) y1))))) H_y z0 (minus_n_O 
+z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda (n: nat).((le x2 
+z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (eq nat (plus 
+x2 (S y2)) y1))))) H2 (S (plus z0 y2)) (plus_n_Sm z0 y2)) in (let H4 \def 
+(eq_ind_r nat (plus x2 (S y2)) (\lambda (n: nat).((le x2 z0) \to ((le O z0) 
+\to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1))))) 
+H3 (S (plus x2 y2)) (plus_n_Sm x2 y2)) in (H4 (le_S_n x2 z0 H) (le_O_n z0) 
+H1)))))))))) (\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall 
+(y2: nat).((le (S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus 
+z0 x2) y1) (plus (match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow 
+(minus z0 l)]) y2)) \to (eq nat (S (plus x2 y2)) (plus x4 
+y1))))))))).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S 
+z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0 
+x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4 
+y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) 
+x1)))) z).
+
+lemma le_S_minus:

  \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to 
 (le d (S (minus n h))))))
 \def
  \lambda (d: nat).(\lambda (h: nat).(\lambda (n: nat).(\lambda (H: (le (plus 
  \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to 
 (le d (S (minus n h))))))
 \def
  \lambda (d: nat).(\lambda (h: nat).(\lambda (n: nat).(\lambda (H: (le (plus 

-d h) n)).(let TMP_1 \def (plus d h) in (let TMP_2 \def (le_plus_l d h) in 
-(let H0 \def (le_trans d TMP_1 n TMP_2 H) in (let TMP_3 \def (\lambda (n0: 
-nat).(le d n0)) in (let TMP_4 \def (minus n h) in (let TMP_5 \def (plus TMP_4 
-h) in (let TMP_6 \def (plus d h) in (let TMP_7 \def (le_plus_r d h) in (let 
-TMP_8 \def (le_trans h TMP_6 n TMP_7 H) in (let TMP_9 \def (le_plus_minus_sym 
-h n TMP_8) in (let H1 \def (eq_ind nat n TMP_3 H0 TMP_5 TMP_9) in (let TMP_10 
-\def (minus n h) in (let TMP_11 \def (le_minus d n h H) in (le_S d TMP_10 
-TMP_11))))))))))))))))).
-
-theorem lt_x_pred_y:
+d h) n)).(let H0 \def (le_trans d (plus d h) n (le_plus_l d h) H) in (let H1 
+\def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus 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))))))).
+
+lemma lt_x_pred_y:

  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
 \def
  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
 \def

- \lambda (x: nat).(\lambda (y: nat).(let TMP_2 \def (\lambda (n: nat).((lt x 
-(pred n)) \to (let TMP_1 \def (S x) in (lt TMP_1 n)))) in (let TMP_5 \def 
-(\lambda (H: (lt x O)).(let TMP_3 \def (S x) in (let TMP_4 \def (lt TMP_3 O) 
-in (lt_x_O x H TMP_4)))) in (let TMP_6 \def (\lambda (n: nat).(\lambda (_: 
-(((lt x (pred n)) \to (lt (S x) n)))).(\lambda (H0: (lt x n)).(lt_n_S x n 
-H0)))) in (nat_ind TMP_2 TMP_5 TMP_6 y))))).
+ \lambda (x: nat).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((lt x (pred 
+n)) \to (lt (S x) n))) (\lambda (H: (lt x O)).(lt_x_O x H (lt (S x) O))) 
+(\lambda (n: nat).(\lambda (_: (((lt x (pred n)) \to (lt (S x) n)))).(\lambda 
+(H0: (lt x n)).(lt_n_S x n H0)))) y)).