-nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) in (let TMP_722 \def
-(minus_n_O z0) in (let H2 \def (eq_ind_r nat TMP_724 TMP_723 H_y z0 TMP_722)
-in (let TMP_729 \def (le_O_n z0) in (let TMP_728 \def (le_O_n z0) in (let
-TMP_726 \def (plus z0 y1) in (let TMP_725 \def (plus z0 y2) in (let TMP_727
-\def (eq_add_S TMP_726 TMP_725 H1) in (H2 y1 y2 TMP_729 TMP_728
-TMP_727)))))))))))))))) in (let TMP_721 \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_699 \def (S y1) in (let H_y \def (IH O x3 TMP_699) in (let
-TMP_704 \def (minus z0 O) in (let TMP_703 \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_701 \def (S y1) in (let TMP_702 \def (plus x3
-TMP_701) in (eq nat y3 TMP_702)))))))) in (let TMP_700 \def (minus_n_O z0) in
-(let H2 \def (eq_ind_r nat TMP_704 TMP_703 H_y z0 TMP_700) in (let TMP_711
-\def (S y1) in (let TMP_712 \def (plus z0 TMP_711) in (let TMP_710 \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_708 \def (S y1) in (let TMP_709 \def
-(plus x3 TMP_708) in (eq nat y3 TMP_709)))))))) in (let TMP_706 \def (plus z0
-y1) in (let TMP_707 \def (S TMP_706) in (let TMP_705 \def (plus_n_Sm z0 y1)
-in (let H3 \def (eq_ind_r nat TMP_712 TMP_710 H2 TMP_707 TMP_705) in (let
-TMP_717 \def (S y1) in (let TMP_718 \def (plus x3 TMP_717) in (let TMP_716
-\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_714 \def (plus x3 y1) in (let TMP_715 \def (S TMP_714) in (let TMP_713
-\def (plus_n_Sm x3 y1) in (let H4 \def (eq_ind_r nat TMP_718 TMP_716 H3
-TMP_715 TMP_713) in (let TMP_720 \def (le_O_n z0) in (let TMP_719 \def
-(le_S_n x3 z0 H0) in (H4 y2 TMP_720 TMP_719 H1))))))))))))))))))))))))))))))
-in (nat_ind TMP_733 TMP_730 TMP_721 x2))))) in (let TMP_698 \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 (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_697 \def (\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)) \to (let
-TMP_695 \def (S x2) in (let TMP_696 \def (plus TMP_695 y2) in (let TMP_694
-\def (plus n y1) in (eq nat TMP_696 TMP_694)))))))))) in (let TMP_693 \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_671 \def (S y2) in (let H_y \def (IH x2 O y1
-TMP_671) in (let TMP_676 \def (minus z0 O) in (let TMP_675 \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_673 \def (S y2) in (let TMP_674 \def (plus x2 TMP_673)
-in (eq nat TMP_674 y1))))))) in (let TMP_672 \def (minus_n_O z0) in (let H2
-\def (eq_ind_r nat TMP_676 TMP_675 H_y z0 TMP_672) in (let TMP_683 \def (S
-y2) in (let TMP_684 \def (plus z0 TMP_683) in (let TMP_682 \def (\lambda (n:
-nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to
-(let TMP_680 \def (S y2) in (let TMP_681 \def (plus x2 TMP_680) in (eq nat
-TMP_681 y1))))))) in (let TMP_678 \def (plus z0 y2) in (let TMP_679 \def (S
-TMP_678) in (let TMP_677 \def (plus_n_Sm z0 y2) in (let H3 \def (eq_ind_r nat
-TMP_684 TMP_682 H2 TMP_679 TMP_677) in (let TMP_689 \def (S y2) in (let
-TMP_690 \def (plus x2 TMP_689) in (let TMP_688 \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_686 \def (plus x2 y2) in (let TMP_687 \def (S
-TMP_686) in (let TMP_685 \def (plus_n_Sm x2 y2) in (let H4 \def (eq_ind_r nat
-TMP_690 TMP_688 H3 TMP_687 TMP_685) in (let TMP_692 \def (le_S_n x2 z0 H) in
-(let TMP_691 \def (le_O_n z0) in (H4 TMP_692 TMP_691
-H1)))))))))))))))))))))))))))) in (let TMP_670 \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_669 \def (plus x2 y2) in (let TMP_668 \def (plus x4 y1) in
-(let TMP_666 \def (le_S_n x2 z0 H) in (let TMP_665 \def (le_S_n x4 z0 H0) in
-(let TMP_667 \def (IH x2 x4 y1 y2 TMP_666 TMP_665 H1) in (f_equal nat nat S
-TMP_669 TMP_668 TMP_667))))))))))))) in (nat_ind TMP_697 TMP_693 TMP_670
-x3))))))) in (nat_ind TMP_737 TMP_734 TMP_698 x1))))))) in (nat_ind TMP_755
-TMP_752 TMP_738 z)))).
-
-theorem le_S_minus:
+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
+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))
+\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: