- \lambda (n: nat).(\lambda (m: nat).(let TMP_3 \def (\lambda (n0:
-nat).(\lambda (n1: nat).(let TMP_1 \def (le n0 n1) in (let TMP_2 \def (lt n1
-n0) in (or TMP_1 TMP_2))))) in (let TMP_7 \def (\lambda (n0: nat).(let TMP_4
-\def (le O n0) in (let TMP_5 \def (lt n0 O) in (let TMP_6 \def (le_O_n n0) in
-(or_introl TMP_4 TMP_5 TMP_6))))) in (let TMP_15 \def (\lambda (n0: nat).(let
-TMP_8 \def (S n0) in (let TMP_9 \def (le TMP_8 O) in (let TMP_10 \def (S n0)
-in (let TMP_11 \def (lt O TMP_10) in (let TMP_12 \def (S n0) in (let TMP_13
-\def (lt_O_Sn n0) in (let TMP_14 \def (lt_le_S O TMP_12 TMP_13) in (or_intror
-TMP_9 TMP_11 TMP_14))))))))) in (let TMP_42 \def (\lambda (n0: nat).(\lambda
-(m0: nat).(\lambda (H: (or (le n0 m0) (lt m0 n0))).(let TMP_16 \def (le n0
-m0) in (let TMP_17 \def (lt m0 n0) in (let TMP_18 \def (S n0) in (let TMP_19
-\def (S m0) in (let TMP_20 \def (le TMP_18 TMP_19) in (let TMP_21 \def (S m0)
-in (let TMP_22 \def (S n0) in (let TMP_23 \def (lt TMP_21 TMP_22) in (let
-TMP_24 \def (or TMP_20 TMP_23) in (let TMP_32 \def (\lambda (H0: (le n0
-m0)).(let TMP_25 \def (S n0) in (let TMP_26 \def (S m0) in (let TMP_27 \def
-(le TMP_25 TMP_26) in (let TMP_28 \def (S m0) in (let TMP_29 \def (S n0) in
-(let TMP_30 \def (lt TMP_28 TMP_29) in (let TMP_31 \def (le_n_S n0 m0 H0) in
-(or_introl TMP_27 TMP_30 TMP_31))))))))) in (let TMP_41 \def (\lambda (H0:
-(lt m0 n0)).(let TMP_33 \def (S n0) in (let TMP_34 \def (S m0) in (let TMP_35
-\def (le TMP_33 TMP_34) in (let TMP_36 \def (S m0) in (let TMP_37 \def (S n0)
-in (let TMP_38 \def (lt TMP_36 TMP_37) in (let TMP_39 \def (S m0) in (let
-TMP_40 \def (le_n_S TMP_39 n0 H0) in (or_intror TMP_35 TMP_38
-TMP_40)))))))))) in (or_ind TMP_16 TMP_17 TMP_24 TMP_32 TMP_41
-H))))))))))))))) in (nat_double_ind TMP_3 TMP_7 TMP_15 TMP_42 n m)))))).
-
-theorem plus_n_O:
+ \lambda (n: nat).(\lambda (m: nat).(nat_double_ind (\lambda (n0:
+nat).(\lambda (n1: nat).(or (le n0 n1) (lt n1 n0)))) (\lambda (n0:
+nat).(or_introl (le O n0) (lt n0 O) (le_O_n n0))) (\lambda (n0:
+nat).(or_intror (le (S n0) O) (lt O (S n0)) (lt_le_S O (S n0) (lt_O_Sn n0))))
+(\lambda (n0: nat).(\lambda (m0: nat).(\lambda (H: (or (le n0 m0) (lt m0
+n0))).(or_ind (le n0 m0) (lt m0 n0) (or (le (S n0) (S m0)) (lt (S m0) (S
+n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S
+n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S
+m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
+
+lemma plus_n_O: