matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "ground_1/preamble.ma".
  18
  19 theorem nat_dec:
  20  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to
  21 (\forall (P: Prop).P))))
  22 \def
  23  \lambda (n1: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (n2: nat).(let
  24 TMP_1 \def (eq nat n n2) in (let TMP_2 \def ((eq nat n n2) \to (\forall (P:
  25 Prop).P)) in (or TMP_1 TMP_2))))) in (let TMP_18 \def (\lambda (n2: nat).(let
  26 TMP_6 \def (\lambda (n: nat).(let TMP_4 \def (eq nat O n) in (let TMP_5 \def
  27 ((eq nat O n) \to (\forall (P: Prop).P)) in (or TMP_4 TMP_5)))) in (let TMP_7
  28 \def (eq nat O O) in (let TMP_8 \def ((eq nat O O) \to (\forall (P: Prop).P))
  29 in (let TMP_9 \def (refl_equal nat O) in (let TMP_10 \def (or_introl TMP_7
  30 TMP_8 TMP_9) in (let TMP_17 \def (\lambda (n: nat).(\lambda (_: (or (eq nat O
  31 n) ((eq nat O n) \to (\forall (P: Prop).P)))).(let TMP_11 \def (S n) in (let
  32 TMP_12 \def (eq nat O TMP_11) in (let TMP_13 \def ((eq nat O (S n)) \to
  33 (\forall (P: Prop).P)) in (let TMP_16 \def (\lambda (H0: (eq nat O (S
  34 n))).(\lambda (P: Prop).(let TMP_14 \def (\lambda (ee: nat).(match ee with [O
  35 \Rightarrow True | (S _) \Rightarrow False])) in (let TMP_15 \def (S n) in
  36 (let H1 \def (eq_ind nat O TMP_14 I TMP_15 H0) in (False_ind P H1)))))) in
  37 (or_intror TMP_12 TMP_13 TMP_16))))))) in (nat_ind TMP_6 TMP_10 TMP_17
  38 n2)))))))) in (let TMP_71 \def (\lambda (n: nat).(\lambda (H: ((\forall (n2:
  39 nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda
  40 (n2: nat).(let TMP_22 \def (\lambda (n0: nat).(let TMP_19 \def (S n) in (let
  41 TMP_20 \def (eq nat TMP_19 n0) in (let TMP_21 \def ((eq nat (S n) n0) \to
  42 (\forall (P: Prop).P)) in (or TMP_20 TMP_21))))) in (let TMP_23 \def (S n) in
  43 (let TMP_24 \def (eq nat TMP_23 O) in (let TMP_25 \def ((eq nat (S n) O) \to
  44 (\forall (P: Prop).P)) in (let TMP_28 \def (\lambda (H0: (eq nat (S n)
  45 O)).(\lambda (P: Prop).(let TMP_26 \def (S n) in (let TMP_27 \def (\lambda
  46 (ee: nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow True])) in
  47 (let H1 \def (eq_ind nat TMP_26 TMP_27 I O H0) in (False_ind P H1)))))) in
  48 (let TMP_29 \def (or_intror TMP_24 TMP_25 TMP_28) in (let TMP_70 \def
  49 (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to
  50 (\forall (P: Prop).P)))).(let TMP_30 \def (eq nat n n0) in (let TMP_31 \def
  51 ((eq nat n n0) \to (\forall (P: Prop).P)) in (let TMP_32 \def (S n) in (let
  52 TMP_33 \def (S n0) in (let TMP_34 \def (eq nat TMP_32 TMP_33) in (let TMP_35
  53 \def ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_36 \def
  54 (or TMP_34 TMP_35) in (let TMP_53 \def (\lambda (H1: (eq nat n n0)).(let
  55 TMP_40 \def (\lambda (n3: nat).(let TMP_37 \def (S n) in (let TMP_38 \def (eq
  56 nat TMP_37 n3) in (let TMP_39 \def ((eq nat (S n) n3) \to (\forall (P:
  57 Prop).P)) in (or TMP_38 TMP_39))))) in (let H2 \def (eq_ind_r nat n0 TMP_40
  58 H0 n H1) in (let TMP_45 \def (\lambda (n3: nat).(let TMP_41 \def (S n) in
  59 (let TMP_42 \def (S n3) in (let TMP_43 \def (eq nat TMP_41 TMP_42) in (let
  60 TMP_44 \def ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)) in (or TMP_43
  61 TMP_44)))))) in (let TMP_46 \def (S n) in (let TMP_47 \def (S n) in (let
  62 TMP_48 \def (eq nat TMP_46 TMP_47) in (let TMP_49 \def ((eq nat (S n) (S n))
  63 \to (\forall (P: Prop).P)) in (let TMP_50 \def (S n) in (let TMP_51 \def
  64 (refl_equal nat TMP_50) in (let TMP_52 \def (or_introl TMP_48 TMP_49 TMP_51)
  65 in (eq_ind nat n TMP_45 TMP_52 n0 H1)))))))))))) in (let TMP_68 \def (\lambda
  66 (H1: (((eq nat n n0) \to (\forall (P: Prop).P)))).(let TMP_54 \def (S n) in
  67 (let TMP_55 \def (S n0) in (let TMP_56 \def (eq nat TMP_54 TMP_55) in (let
  68 TMP_57 \def ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P)) in (let TMP_67
  69 \def (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P: Prop).(let TMP_58 \def
  70 (\lambda (e: nat).(match e with [O \Rightarrow n | (S n3) \Rightarrow n3]))
  71 in (let TMP_59 \def (S n) in (let TMP_60 \def (S n0) in (let H3 \def (f_equal
  72 nat nat TMP_58 TMP_59 TMP_60 H2) in (let TMP_61 \def (\lambda (n3: nat).((eq
  73 nat n n3) \to (\forall (P0: Prop).P0))) in (let H4 \def (eq_ind_r nat n0
  74 TMP_61 H1 n H3) in (let TMP_65 \def (\lambda (n3: nat).(let TMP_62 \def (S n)
  75 in (let TMP_63 \def (eq nat TMP_62 n3) in (let TMP_64 \def ((eq nat (S n) n3)
  76 \to (\forall (P0: Prop).P0)) in (or TMP_63 TMP_64))))) in (let H5 \def
  77 (eq_ind_r nat n0 TMP_65 H0 n H3) in (let TMP_66 \def (refl_equal nat n) in
  78 (H4 TMP_66 P)))))))))))) in (or_intror TMP_56 TMP_57 TMP_67))))))) in (let
  79 TMP_69 \def (H n0) in (or_ind TMP_30 TMP_31 TMP_36 TMP_53 TMP_68
  80 TMP_69))))))))))))) in (nat_ind TMP_22 TMP_29 TMP_70 n2))))))))))) in
  81 (nat_ind TMP_3 TMP_18 TMP_71 n1)))).
  82
  83 theorem simpl_plus_r:
  84  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n)
  85 (plus p n)) \to (eq nat m p))))
  86 \def
  87  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat
  88 (plus m n) (plus p n))).(let TMP_1 \def (plus m n) in (let TMP_3 \def
  89 (\lambda (n0: nat).(let TMP_2 \def (plus n p) in (eq nat n0 TMP_2))) in (let
  90 TMP_4 \def (plus p n) in (let TMP_6 \def (\lambda (n0: nat).(let TMP_5 \def
  91 (plus n p) in (eq nat n0 TMP_5))) in (let TMP_7 \def (plus_sym p n) in (let
  92 TMP_8 \def (plus m n) in (let TMP_9 \def (eq_ind_r nat TMP_4 TMP_6 TMP_7
  93 TMP_8 H) in (let TMP_10 \def (plus n m) in (let TMP_11 \def (plus_sym n m) in
  94 (let TMP_12 \def (eq_ind_r nat TMP_1 TMP_3 TMP_9 TMP_10 TMP_11) in
  95 (simpl_plus_l n m p TMP_12)))))))))))))).
  96
  97 theorem minus_Sx_Sy:
  98  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
  99 \def
 100  \lambda (x: nat).(\lambda (y: nat).(let TMP_1 \def (minus x y) in
 101 (refl_equal nat TMP_1))).
 102
 103 theorem minus_plus_r:
 104  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
 105 \def
 106  \lambda (m: nat).(\lambda (n: nat).(let TMP_1 \def (plus n m) in (let TMP_3
 107 \def (\lambda (n0: nat).(let TMP_2 \def (minus n0 n) in (eq nat TMP_2 m))) in
 108 (let TMP_4 \def (minus_plus n m) in (let TMP_5 \def (plus m n) in (let TMP_6
 109 \def (plus_sym m n) in (eq_ind_r nat TMP_1 TMP_3 TMP_4 TMP_5 TMP_6))))))).
 110
 111 theorem plus_permute_2_in_3:
 112  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x
 113 y) z) (plus (plus x z) y))))
 114 \def
 115  \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(let TMP_1 \def (plus y
 116 z) in (let TMP_2 \def (plus x TMP_1) in (let TMP_5 \def (\lambda (n:
 117 nat).(let TMP_3 \def (plus x z) in (let TMP_4 \def (plus TMP_3 y) in (eq nat
 118 n TMP_4)))) in (let TMP_6 \def (plus z y) in (let TMP_10 \def (\lambda (n:
 119 nat).(let TMP_7 \def (plus x n) in (let TMP_8 \def (plus x z) in (let TMP_9
 120 \def (plus TMP_8 y) in (eq nat TMP_7 TMP_9))))) in (let TMP_11 \def (plus x
 121 z) in (let TMP_12 \def (plus TMP_11 y) in (let TMP_15 \def (\lambda (n:
 122 nat).(let TMP_13 \def (plus x z) in (let TMP_14 \def (plus TMP_13 y) in (eq
 123 nat n TMP_14)))) in (let TMP_16 \def (plus x z) in (let TMP_17 \def (plus
 124 TMP_16 y) in (let TMP_18 \def (refl_equal nat TMP_17) in (let TMP_19 \def
 125 (plus z y) in (let TMP_20 \def (plus x TMP_19) in (let TMP_21 \def
 126 (plus_assoc_r x z y) in (let TMP_22 \def (eq_ind nat TMP_12 TMP_15 TMP_18
 127 TMP_20 TMP_21) in (let TMP_23 \def (plus y z) in (let TMP_24 \def (plus_sym y
 128 z) in (let TMP_25 \def (eq_ind_r nat TMP_6 TMP_10 TMP_22 TMP_23 TMP_24) in
 129 (let TMP_26 \def (plus x y) in (let TMP_27 \def (plus TMP_26 z) in (let
 130 TMP_28 \def (plus_assoc_r x y z) in (eq_ind_r nat TMP_2 TMP_5 TMP_25 TMP_27
 131 TMP_28)))))))))))))))))))))))).
 132
 133 theorem plus_permute_2_in_3_assoc:
 134  \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n
 135 h) k) (plus n (plus k h)))))
 136 \def
 137  \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(let TMP_1 \def (plus n
 138 k) in (let TMP_2 \def (plus TMP_1 h) in (let TMP_5 \def (\lambda (n0:
 139 nat).(let TMP_3 \def (plus k h) in (let TMP_4 \def (plus n TMP_3) in (eq nat
 140 n0 TMP_4)))) in (let TMP_6 \def (plus n k) in (let TMP_7 \def (plus TMP_6 h)
 141 in (let TMP_10 \def (\lambda (n0: nat).(let TMP_8 \def (plus n k) in (let
 142 TMP_9 \def (plus TMP_8 h) in (eq nat TMP_9 n0)))) in (let TMP_11 \def (plus n
 143 k) in (let TMP_12 \def (plus TMP_11 h) in (let TMP_13 \def (refl_equal nat
 144 TMP_12) in (let TMP_14 \def (plus k h) in (let TMP_15 \def (plus n TMP_14) in
 145 (let TMP_16 \def (plus_assoc_l n k h) in (let TMP_17 \def (eq_ind_r nat TMP_7
 146 TMP_10 TMP_13 TMP_15 TMP_16) in (let TMP_18 \def (plus n h) in (let TMP_19
 147 \def (plus TMP_18 k) in (let TMP_20 \def (plus_permute_2_in_3 n h k) in
 148 (eq_ind_r nat TMP_2 TMP_5 TMP_17 TMP_19 TMP_20))))))))))))))))))).
 149
 150 theorem plus_O:
 151  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat
 152 x O) (eq nat y O))))
 153 \def
 154  \lambda (x: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (y: nat).((eq
 155 nat (plus n y) O) \to (let TMP_1 \def (eq nat n O) in (let TMP_2 \def (eq nat
 156 y O) in (land TMP_1 TMP_2)))))) in (let TMP_7 \def (\lambda (y: nat).(\lambda
 157 (H: (eq nat (plus O y) O)).(let TMP_4 \def (eq nat O O) in (let TMP_5 \def
 158 (eq nat y O) in (let TMP_6 \def (refl_equal nat O) in (conj TMP_4 TMP_5 TMP_6
 159 H)))))) in (let TMP_16 \def (\lambda (n: nat).(\lambda (_: ((\forall (y:
 160 nat).((eq nat (plus n y) O) \to (land (eq nat n O) (eq nat y O)))))).(\lambda
 161 (y: nat).(\lambda (H0: (eq nat (plus (S n) y) O)).(let H1 \def (match H0 with
 162 [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let TMP_8
 163 \def (S n) in (let TMP_9 \def (plus TMP_8 y) in (let TMP_10 \def (\lambda (e:
 164 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) in (let
 165 H2 \def (eq_ind nat TMP_9 TMP_10 I O H1) in (let TMP_11 \def (S n) in (let
 166 TMP_12 \def (eq nat TMP_11 O) in (let TMP_13 \def (eq nat y O) in (let TMP_14
 167 \def (land TMP_12 TMP_13) in (False_ind TMP_14 H2))))))))))]) in (let TMP_15
 168 \def (refl_equal nat O) in (H1 TMP_15))))))) in (nat_ind TMP_3 TMP_7 TMP_16
 169 x)))).
 170
 171 theorem minus_Sx_SO:
 172  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
 173 \def
 174  \lambda (x: nat).(let TMP_1 \def (\lambda (n: nat).(eq nat n x)) in (let
 175 TMP_2 \def (refl_equal nat x) in (let TMP_3 \def (minus x O) in (let TMP_4
 176 \def (minus_n_O x) in (eq_ind nat x TMP_1 TMP_2 TMP_3 TMP_4))))).
 177
 178 theorem nat_dec_neg:
 179  \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
 180 \def
 181  \lambda (i: nat).(let TMP_4 \def (\lambda (n: nat).(\forall (j: nat).(let
 182 TMP_1 \def (eq nat n j) in (let TMP_2 \def (not TMP_1) in (let TMP_3 \def (eq
 183 nat n j) in (or TMP_2 TMP_3)))))) in (let TMP_21 \def (\lambda (j: nat).(let
 184 TMP_8 \def (\lambda (n: nat).(let TMP_5 \def (eq nat O n) in (let TMP_6 \def
 185 (not TMP_5) in (let TMP_7 \def (eq nat O n) in (or TMP_6 TMP_7))))) in (let
 186 TMP_9 \def (eq nat O O) in (let TMP_10 \def (not TMP_9) in (let TMP_11 \def
 187 (eq nat O O) in (let TMP_12 \def (refl_equal nat O) in (let TMP_13 \def
 188 (or_intror TMP_10 TMP_11 TMP_12) in (let TMP_20 \def (\lambda (n:
 189 nat).(\lambda (_: (or (not (eq nat O n)) (eq nat O n))).(let TMP_14 \def (S
 190 n) in (let TMP_15 \def (eq nat O TMP_14) in (let TMP_16 \def (not TMP_15) in
 191 (let TMP_17 \def (S n) in (let TMP_18 \def (eq nat O TMP_17) in (let TMP_19
 192 \def (O_S n) in (or_introl TMP_16 TMP_18 TMP_19))))))))) in (nat_ind TMP_8
 193 TMP_13 TMP_20 j))))))))) in (let TMP_68 \def (\lambda (n: nat).(\lambda (H:
 194 ((\forall (j: nat).(or (not (eq nat n j)) (eq nat n j))))).(\lambda (j:
 195 nat).(let TMP_27 \def (\lambda (n0: nat).(let TMP_22 \def (S n) in (let
 196 TMP_23 \def (eq nat TMP_22 n0) in (let TMP_24 \def (not TMP_23) in (let
 197 TMP_25 \def (S n) in (let TMP_26 \def (eq nat TMP_25 n0) in (or TMP_24
 198 TMP_26))))))) in (let TMP_28 \def (S n) in (let TMP_29 \def (eq nat TMP_28 O)
 199 in (let TMP_30 \def (not TMP_29) in (let TMP_31 \def (S n) in (let TMP_32
 200 \def (eq nat TMP_31 O) in (let TMP_33 \def (S n) in (let TMP_34 \def (O_S n)
 201 in (let TMP_35 \def (sym_not_eq nat O TMP_33 TMP_34) in (let TMP_36 \def
 202 (or_introl TMP_30 TMP_32 TMP_35) in (let TMP_67 \def (\lambda (n0:
 203 nat).(\lambda (_: (or (not (eq nat (S n) n0)) (eq nat (S n) n0))).(let TMP_37
 204 \def (eq nat n n0) in (let TMP_38 \def (not TMP_37) in (let TMP_39 \def (eq
 205 nat n n0) in (let TMP_40 \def (S n) in (let TMP_41 \def (S n0) in (let TMP_42
 206 \def (eq nat TMP_40 TMP_41) in (let TMP_43 \def (not TMP_42) in (let TMP_44
 207 \def (S n) in (let TMP_45 \def (S n0) in (let TMP_46 \def (eq nat TMP_44
 208 TMP_45) in (let TMP_47 \def (or TMP_43 TMP_46) in (let TMP_56 \def (\lambda
 209 (H1: (not (eq nat n n0))).(let TMP_48 \def (S n) in (let TMP_49 \def (S n0)
 210 in (let TMP_50 \def (eq nat TMP_48 TMP_49) in (let TMP_51 \def (not TMP_50)
 211 in (let TMP_52 \def (S n) in (let TMP_53 \def (S n0) in (let TMP_54 \def (eq
 212 nat TMP_52 TMP_53) in (let TMP_55 \def (not_eq_S n n0 H1) in (or_introl
 213 TMP_51 TMP_54 TMP_55)))))))))) in (let TMP_65 \def (\lambda (H1: (eq nat n
 214 n0)).(let TMP_57 \def (S n) in (let TMP_58 \def (S n0) in (let TMP_59 \def
 215 (eq nat TMP_57 TMP_58) in (let TMP_60 \def (not TMP_59) in (let TMP_61 \def
 216 (S n) in (let TMP_62 \def (S n0) in (let TMP_63 \def (eq nat TMP_61 TMP_62)
 217 in (let TMP_64 \def (f_equal nat nat S n n0 H1) in (or_intror TMP_60 TMP_63
 218 TMP_64)))))))))) in (let TMP_66 \def (H n0) in (or_ind TMP_38 TMP_39 TMP_47
 219 TMP_56 TMP_65 TMP_66))))))))))))))))) in (nat_ind TMP_27 TMP_36 TMP_67
 220 j))))))))))))))) in (nat_ind TMP_4 TMP_21 TMP_68 i)))).
 221
 222 theorem neq_eq_e:
 223  \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j))
 224 \to P)) \to ((((eq nat i j) \to P)) \to P))))
 225 \def
 226  \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not
 227 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def
 228 (nat_dec_neg i j) in (let TMP_1 \def (eq nat i j) in (let TMP_2 \def (not
 229 TMP_1) in (let TMP_3 \def (eq nat i j) in (or_ind TMP_2 TMP_3 P H H0
 230 o))))))))).
 231
 232 theorem le_false:
 233  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S
 234 n) m) \to P))))
 235 \def
 236  \lambda (m: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (n0:
 237 nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P))))) in (let
 238 TMP_9 \def (\lambda (n: nat).(\lambda (P: Prop).(\lambda (_: (le O
 239 n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 with [le_n \Rightarrow
 240 (\lambda (H1: (eq nat (S n) O)).(let TMP_6 \def (S n) in (let TMP_7 \def
 241 (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
 242 True])) in (let H2 \def (eq_ind nat TMP_6 TMP_7 I O H1) in (False_ind P
 243 H2))))) | (le_S m0 H1) \Rightarrow (\lambda (H2: (eq nat (S m0) O)).(let
 244 TMP_2 \def (S m0) in (let TMP_3 \def (\lambda (e: nat).(match e with [O
 245 \Rightarrow False | (S _) \Rightarrow True])) in (let H3 \def (eq_ind nat
 246 TMP_2 TMP_3 I O H2) in (let TMP_4 \def ((le (S n) m0) \to P) in (let TMP_5
 247 \def (False_ind TMP_4 H3) in (TMP_5 H1)))))))]) in (let TMP_8 \def
 248 (refl_equal nat O) in (H1 TMP_8))))))) in (let TMP_23 \def (\lambda (n:
 249 nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le
 250 (S n0) n) \to P)))))).(\lambda (n0: nat).(let TMP_10 \def (\lambda (n1:
 251 nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P)))) in
 252 (let TMP_18 \def (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_:
 253 (le (S O) (S n))).(let H2 \def (match H0 with [le_n \Rightarrow (\lambda (H2:
 254 (eq nat (S n) O)).(let TMP_15 \def (S n) in (let TMP_16 \def (\lambda (e:
 255 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) in (let
 256 H3 \def (eq_ind nat TMP_15 TMP_16 I O H2) in (False_ind P H3))))) | (le_S m0
 257 H2) \Rightarrow (\lambda (H3: (eq nat (S m0) O)).(let TMP_11 \def (S m0) in
 258 (let TMP_12 \def (\lambda (e: nat).(match e with [O \Rightarrow False | (S _)
 259 \Rightarrow True])) in (let H4 \def (eq_ind nat TMP_11 TMP_12 I O H3) in (let
 260 TMP_13 \def ((le (S n) m0) \to P) in (let TMP_14 \def (False_ind TMP_13 H4)
 261 in (TMP_14 H2)))))))]) in (let TMP_17 \def (refl_equal nat O) in (H2
 262 TMP_17)))))) in (let TMP_22 \def (\lambda (n1: nat).(\lambda (_: ((\forall
 263 (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P:
 264 Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S
 265 n))).(let TMP_19 \def (le_S_n n n1 H1) in (let TMP_20 \def (S n1) in (let
 266 TMP_21 \def (le_S_n TMP_20 n H2) in (H n1 P TMP_19 TMP_21))))))))) in
 267 (nat_ind TMP_10 TMP_18 TMP_22 n0))))))) in (nat_ind TMP_1 TMP_9 TMP_23 m)))).
 268
 269 theorem le_Sx_x:
 270  \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
 271 \def
 272  \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def
 273 le_Sn_n in (let TMP_1 \def (H0 x H) in (False_ind P TMP_1))))).
 274
 275 theorem le_n_pred:
 276  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
 277 \def
 278  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(let TMP_3 \def
 279 (\lambda (n0: nat).(let TMP_1 \def (pred n) in (let TMP_2 \def (pred n0) in
 280 (le TMP_1 TMP_2)))) in (let TMP_4 \def (pred n) in (let TMP_5 \def (le_n
 281 TMP_4) in (let TMP_9 \def (\lambda (m0: nat).(\lambda (_: (le n m0)).(\lambda
 282 (H1: (le (pred n) (pred m0))).(let TMP_6 \def (pred n) in (let TMP_7 \def
 283 (pred m0) in (let TMP_8 \def (le_pred_n m0) in (le_trans TMP_6 TMP_7 m0 H1
 284 TMP_8))))))) in (le_ind n TMP_3 TMP_5 TMP_9 m H))))))).
 285
 286 theorem minus_le:
 287  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
 288 \def
 289  \lambda (x: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (y: nat).(let
 290 TMP_1 \def (minus n y) in (le TMP_1 n)))) in (let TMP_3 \def (\lambda (_:
 291 nat).(le_O_n O)) in (let TMP_13 \def (\lambda (n: nat).(\lambda (H: ((\forall
 292 (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(let TMP_7 \def (\lambda
 293 (n0: nat).(let TMP_4 \def (S n) in (let TMP_5 \def (minus TMP_4 n0) in (let
 294 TMP_6 \def (S n) in (le TMP_5 TMP_6))))) in (let TMP_8 \def (S n) in (let
 295 TMP_9 \def (le_n TMP_8) in (let TMP_12 \def (\lambda (n0: nat).(\lambda (_:
 296 (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)]) (S
 297 n))).(let TMP_10 \def (minus n n0) in (let TMP_11 \def (H n0) in (le_S TMP_10
 298 n TMP_11))))) in (nat_ind TMP_7 TMP_9 TMP_12 y)))))))) in (nat_ind TMP_2
 299 TMP_3 TMP_13 x)))).
 300
 301 theorem le_plus_minus_sym:
 302  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n)
 303 n))))
 304 \def
 305  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(let TMP_1 \def
 306 (minus m n) in (let TMP_2 \def (plus n TMP_1) in (let TMP_3 \def (\lambda
 307 (n0: nat).(eq nat m n0)) in (let TMP_4 \def (le_plus_minus n m H) in (let
 308 TMP_5 \def (minus m n) in (let TMP_6 \def (plus TMP_5 n) in (let TMP_7 \def
 309 (minus m n) in (let TMP_8 \def (plus_sym TMP_7 n) in (eq_ind_r nat TMP_2
 310 TMP_3 TMP_4 TMP_6 TMP_8))))))))))).
 311
 312 theorem le_minus_minus:
 313  \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z)
 314 \to (le (minus y x) (minus z x))))))
 315 \def
 316  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z:
 317 nat).(\lambda (H0: (le y z)).(let TMP_1 \def (minus y x) in (let TMP_2 \def
 318 (minus z x) in (let TMP_5 \def (\lambda (n: nat).(let TMP_3 \def (minus z x)
 319 in (let TMP_4 \def (plus x TMP_3) in (le n TMP_4)))) in (let TMP_6 \def
 320 (\lambda (n: nat).(le y n)) in (let TMP_7 \def (minus z x) in (let TMP_8 \def
 321 (plus x TMP_7) in (let TMP_9 \def (le_trans x y z H H0) in (let TMP_10 \def
 322 (le_plus_minus_r x z TMP_9) in (let TMP_11 \def (eq_ind_r nat z TMP_6 H0
 323 TMP_8 TMP_10) in (let TMP_12 \def (minus y x) in (let TMP_13 \def (plus x
 324 TMP_12) in (let TMP_14 \def (le_plus_minus_r x y H) in (let TMP_15 \def
 325 (eq_ind_r nat y TMP_5 TMP_11 TMP_13 TMP_14) in (simpl_le_plus_l x TMP_1 TMP_2
 326 TMP_15)))))))))))))))))).
 327
 328 theorem le_minus_plus:
 329  \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat
 330 (minus (plus x y) z) (plus (minus x z) y)))))
 331 \def
 332  \lambda (z: nat).(let TMP_5 \def (\lambda (n: nat).(\forall (x: nat).((le n
 333 x) \to (\forall (y: nat).(let TMP_1 \def (plus x y) in (let TMP_2 \def (minus
 334 TMP_1 n) in (let TMP_3 \def (minus x n) in (let TMP_4 \def (plus TMP_3 y) in
 335 (eq nat TMP_2 TMP_4))))))))) in (let TMP_29 \def (\lambda (x: nat).(\lambda
 336 (H: (le O x)).(let H0 \def (match H with [le_n \Rightarrow (\lambda (H0: (eq
 337 nat O x)).(let TMP_20 \def (\lambda (n: nat).(\forall (y: nat).(let TMP_16
 338 \def (plus n y) in (let TMP_17 \def (minus TMP_16 O) in (let TMP_18 \def
 339 (minus n O) in (let TMP_19 \def (plus TMP_18 y) in (eq nat TMP_17
 340 TMP_19))))))) in (let TMP_27 \def (\lambda (y: nat).(let TMP_21 \def (minus O
 341 O) in (let TMP_22 \def (plus TMP_21 y) in (let TMP_23 \def (plus O y) in (let
 342 TMP_24 \def (minus TMP_23 O) in (let TMP_25 \def (plus O y) in (let TMP_26
 343 \def (minus_n_O TMP_25) in (sym_eq nat TMP_22 TMP_24 TMP_26)))))))) in
 344 (eq_ind nat O TMP_20 TMP_27 x H0)))) | (le_S m H0) \Rightarrow (\lambda (H1:
 345 (eq nat (S m) x)).(let TMP_6 \def (S m) in (let TMP_11 \def (\lambda (n:
 346 nat).((le O m) \to (\forall (y: nat).(let TMP_7 \def (plus n y) in (let TMP_8
 347 \def (minus TMP_7 O) in (let TMP_9 \def (minus n O) in (let TMP_10 \def (plus
 348 TMP_9 y) in (eq nat TMP_8 TMP_10)))))))) in (let TMP_15 \def (\lambda (_: (le
 349 O m)).(\lambda (y: nat).(let TMP_12 \def (S m) in (let TMP_13 \def (minus
 350 TMP_12 O) in (let TMP_14 \def (plus TMP_13 y) in (refl_equal nat TMP_14))))))
 351 in (eq_ind nat TMP_6 TMP_11 TMP_15 x H1 H0)))))]) in (let TMP_28 \def
 352 (refl_equal nat x) in (H0 TMP_28))))) in (let TMP_60 \def (\lambda (z0:
 353 nat).(\lambda (H: ((\forall (x: nat).((le z0 x) \to (\forall (y: nat).(eq nat
 354 (minus (plus x y) z0) (plus (minus x z0) y))))))).(\lambda (x: nat).(let
 355 TMP_36 \def (\lambda (n: nat).((le (S z0) n) \to (\forall (y: nat).(let
 356 TMP_30 \def (plus n y) in (let TMP_31 \def (S z0) in (let TMP_32 \def (minus
 357 TMP_30 TMP_31) in (let TMP_33 \def (S z0) in (let TMP_34 \def (minus n
 358 TMP_33) in (let TMP_35 \def (plus TMP_34 y) in (eq nat TMP_32
 359 TMP_35)))))))))) in (let TMP_57 \def (\lambda (H0: (le (S z0) O)).(\lambda
 360 (y: nat).(let H1 \def (match H0 with [le_n \Rightarrow (\lambda (H1: (eq nat
 361 (S z0) O)).(let TMP_47 \def (S z0) in (let TMP_48 \def (\lambda (e:
 362 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) in (let
 363 H2 \def (eq_ind nat TMP_47 TMP_48 I O H1) in (let TMP_49 \def (plus O y) in
 364 (let TMP_50 \def (S z0) in (let TMP_51 \def (minus TMP_49 TMP_50) in (let
 365 TMP_52 \def (S z0) in (let TMP_53 \def (minus O TMP_52) in (let TMP_54 \def
 366 (plus TMP_53 y) in (let TMP_55 \def (eq nat TMP_51 TMP_54) in (False_ind
 367 TMP_55 H2)))))))))))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m)
 368 O)).(let TMP_37 \def (S m) in (let TMP_38 \def (\lambda (e: nat).(match e
 369 with [O \Rightarrow False | (S _) \Rightarrow True])) in (let H3 \def (eq_ind
 370 nat TMP_37 TMP_38 I O H2) in (let TMP_45 \def ((le (S z0) m) \to (let TMP_39
 371 \def (plus O y) in (let TMP_40 \def (S z0) in (let TMP_41 \def (minus TMP_39
 372 TMP_40) in (let TMP_42 \def (S z0) in (let TMP_43 \def (minus O TMP_42) in
 373 (let TMP_44 \def (plus TMP_43 y) in (eq nat TMP_41 TMP_44)))))))) in (let
 374 TMP_46 \def (False_ind TMP_45 H3) in (TMP_46 H1)))))))]) in (let TMP_56 \def
 375 (refl_equal nat O) in (H1 TMP_56))))) in (let TMP_59 \def (\lambda (n:
 376 nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus
 377 n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S
 378 n))).(\lambda (y: nat).(let TMP_58 \def (le_S_n z0 n H1) in (H n TMP_58
 379 y)))))) in (nat_ind TMP_36 TMP_57 TMP_59 x))))))) in (nat_ind TMP_5 TMP_29
 380 TMP_60 z)))).
 381
 382 theorem le_minus:
 383  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to
 384 (le x (minus z y)))))
 385 \def
 386  \lambda (x: nat).(\lambda (z: nat).(\lambda (y: nat).(\lambda (H: (le (plus
 387 x y) z)).(let TMP_1 \def (plus x y) in (let TMP_2 \def (minus TMP_1 y) in
 388 (let TMP_4 \def (\lambda (n: nat).(let TMP_3 \def (minus z y) in (le n
 389 TMP_3))) in (let TMP_5 \def (plus x y) in (let TMP_6 \def (le_plus_r x y) in
 390 (let TMP_7 \def (le_minus_minus y TMP_5 TMP_6 z H) in (let TMP_8 \def
 391 (minus_plus_r x y) in (eq_ind nat TMP_2 TMP_4 TMP_7 x TMP_8))))))))))).
 392
 393 theorem le_trans_plus_r:
 394  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to
 395 (le y z))))
 396 \def
 397  \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus
 398 x y) z)).(let TMP_1 \def (plus x y) in (let TMP_2 \def (le_plus_r x y) in
 399 (le_trans y TMP_1 z TMP_2 H)))))).
 400
 401 theorem lt_x_O:
 402  \forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
 403 \def
 404  \lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let TMP_1
 405 \def (S x) in (let H_y \def (le_n_O_eq TMP_1 H) in (let TMP_2 \def (\lambda
 406 (ee: nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) in
 407 (let TMP_3 \def (S x) in (let H0 \def (eq_ind nat O TMP_2 I TMP_3 H_y) in
 408 (False_ind P H0)))))))).
 409
 410 theorem le_gen_S:
 411  \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n:
 412 nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
 413 \def
 414  \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def
 415 (match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(let TMP_16
 416 \def (S m) in (let TMP_20 \def (\lambda (n: nat).(let TMP_18 \def (\lambda
 417 (n0: nat).(let TMP_17 \def (S n0) in (eq nat n TMP_17))) in (let TMP_19 \def
 418 (\lambda (n0: nat).(le m n0)) in (ex2 nat TMP_18 TMP_19)))) in (let TMP_23
 419 \def (\lambda (n: nat).(let TMP_21 \def (S m) in (let TMP_22 \def (S n) in
 420 (eq nat TMP_21 TMP_22)))) in (let TMP_24 \def (\lambda (n: nat).(le m n)) in
 421 (let TMP_25 \def (S m) in (let TMP_26 \def (refl_equal nat TMP_25) in (let
 422 TMP_27 \def (le_n m) in (let TMP_28 \def (ex_intro2 nat TMP_23 TMP_24 m
 423 TMP_26 TMP_27) in (eq_ind nat TMP_16 TMP_20 TMP_28 x H0)))))))))) | (le_S m0
 424 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(let TMP_1 \def (S m0) in
 425 (let TMP_5 \def (\lambda (n: nat).((le (S m) m0) \to (let TMP_3 \def (\lambda
 426 (n0: nat).(let TMP_2 \def (S n0) in (eq nat n TMP_2))) in (let TMP_4 \def
 427 (\lambda (n0: nat).(le m n0)) in (ex2 nat TMP_3 TMP_4))))) in (let TMP_15
 428 \def (\lambda (H2: (le (S m) m0)).(let TMP_8 \def (\lambda (n: nat).(let
 429 TMP_6 \def (S m0) in (let TMP_7 \def (S n) in (eq nat TMP_6 TMP_7)))) in (let
 430 TMP_9 \def (\lambda (n: nat).(le m n)) in (let TMP_10 \def (S m0) in (let
 431 TMP_11 \def (refl_equal nat TMP_10) in (let TMP_12 \def (S m) in (let TMP_13
 432 \def (le_S TMP_12 m0 H2) in (let TMP_14 \def (le_S_n m m0 TMP_13) in
 433 (ex_intro2 nat TMP_8 TMP_9 m0 TMP_11 TMP_14))))))))) in (eq_ind nat TMP_1
 434 TMP_5 TMP_15 x H1 H0)))))]) in (let TMP_29 \def (refl_equal nat x) in (H0
 435 TMP_29))))).
 436
 437 theorem lt_x_plus_x_Sy:
 438  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
 439 \def
 440  \lambda (x: nat).(\lambda (y: nat).(let TMP_1 \def (S y) in (let TMP_2 \def
 441 (plus TMP_1 x) in (let TMP_3 \def (\lambda (n: nat).(lt x n)) in (let TMP_4
 442 \def (S x) in (let TMP_5 \def (plus y x) in (let TMP_6 \def (S TMP_5) in (let
 443 TMP_7 \def (S x) in (let TMP_8 \def (plus y x) in (let TMP_9 \def (S TMP_8)
 444 in (let TMP_10 \def (plus y x) in (let TMP_11 \def (le_plus_r y x) in (let
 445 TMP_12 \def (le_n_S x TMP_10 TMP_11) in (let TMP_13 \def (le_n_S TMP_7 TMP_9
 446 TMP_12) in (let TMP_14 \def (le_S_n TMP_4 TMP_6 TMP_13) in (let TMP_15 \def
 447 (S y) in (let TMP_16 \def (plus x TMP_15) in (let TMP_17 \def (S y) in (let
 448 TMP_18 \def (plus_sym x TMP_17) in (eq_ind_r nat TMP_2 TMP_3 TMP_14 TMP_16
 449 TMP_18)))))))))))))))))))).
 450
 451 theorem simpl_lt_plus_r:
 452  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m
 453 p)) \to (lt n m))))
 454 \def
 455  \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus
 456 n p) (plus m p))).(let TMP_1 \def (plus n p) in (let TMP_3 \def (\lambda (n0:
 457 nat).(let TMP_2 \def (plus m p) in (lt n0 TMP_2))) in (let TMP_4 \def (plus p
 458 n) in (let TMP_5 \def (plus_sym n p) in (let H0 \def (eq_ind nat TMP_1 TMP_3
 459 H TMP_4 TMP_5) in (let TMP_6 \def (plus m p) in (let TMP_8 \def (\lambda (n0:
 460 nat).(let TMP_7 \def (plus p n) in (lt TMP_7 n0))) in (let TMP_9 \def (plus p
 461 m) in (let TMP_10 \def (plus_sym m p) in (let H1 \def (eq_ind nat TMP_6 TMP_8
 462 H0 TMP_9 TMP_10) in (simpl_lt_plus_l n m p H1)))))))))))))).
 463
 464 theorem minus_x_Sy:
 465  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S
 466 (minus x (S y))))))
 467 \def
 468  \lambda (x: nat).(let TMP_5 \def (\lambda (n: nat).(\forall (y: nat).((lt y
 469 n) \to (let TMP_1 \def (minus n y) in (let TMP_2 \def (S y) in (let TMP_3
 470 \def (minus n TMP_2) in (let TMP_4 \def (S TMP_3) in (eq nat TMP_1
 471 TMP_4)))))))) in (let TMP_22 \def (\lambda (y: nat).(\lambda (H: (lt y
 472 O)).(let H0 \def (match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S y)
 473 O)).(let TMP_14 \def (S y) in (let TMP_15 \def (\lambda (e: nat).(match e
 474 with [O \Rightarrow False | (S _) \Rightarrow True])) in (let H1 \def (eq_ind
 475 nat TMP_14 TMP_15 I O H0) in (let TMP_16 \def (minus O y) in (let TMP_17 \def
 476 (S y) in (let TMP_18 \def (minus O TMP_17) in (let TMP_19 \def (S TMP_18) in
 477 (let TMP_20 \def (eq nat TMP_16 TMP_19) in (False_ind TMP_20 H1)))))))))) |
 478 (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).(let TMP_6 \def (S m)
 479 in (let TMP_7 \def (\lambda (e: nat).(match e with [O \Rightarrow False | (S
 480 _) \Rightarrow True])) in (let H2 \def (eq_ind nat TMP_6 TMP_7 I O H1) in
 481 (let TMP_12 \def ((le (S y) m) \to (let TMP_8 \def (minus O y) in (let TMP_9
 482 \def (S y) in (let TMP_10 \def (minus O TMP_9) in (let TMP_11 \def (S TMP_10)
 483 in (eq nat TMP_8 TMP_11)))))) in (let TMP_13 \def (False_ind TMP_12 H2) in
 484 (TMP_13 H0)))))))]) in (let TMP_21 \def (refl_equal nat O) in (H0 TMP_21)))))
 485 in (let TMP_40 \def (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y
 486 n) \to (eq nat (minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(let
 487 TMP_29 \def (\lambda (n0: nat).((lt n0 (S n)) \to (let TMP_23 \def (S n) in
 488 (let TMP_24 \def (minus TMP_23 n0) in (let TMP_25 \def (S n) in (let TMP_26
 489 \def (S n0) in (let TMP_27 \def (minus TMP_25 TMP_26) in (let TMP_28 \def (S
 490 TMP_27) in (eq nat TMP_24 TMP_28))))))))) in (let TMP_37 \def (\lambda (_:
 491 (lt O (S n))).(let TMP_32 \def (\lambda (n0: nat).(let TMP_30 \def (S n) in
 492 (let TMP_31 \def (S n0) in (eq nat TMP_30 TMP_31)))) in (let TMP_33 \def (S
 493 n) in (let TMP_34 \def (refl_equal nat TMP_33) in (let TMP_35 \def (minus n
 494 O) in (let TMP_36 \def (minus_n_O n) in (eq_ind nat n TMP_32 TMP_34 TMP_35
 495 TMP_36))))))) in (let TMP_39 \def (\lambda (n0: nat).(\lambda (_: (((lt n0 (S
 496 n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))).(\lambda (H1:
 497 (lt (S n0) (S n))).(let TMP_38 \def (S n0) in (let H2 \def (le_S_n TMP_38 n
 498 H1) in (H n0 H2)))))) in (nat_ind TMP_29 TMP_37 TMP_39 y))))))) in (nat_ind
 499 TMP_5 TMP_22 TMP_40 x)))).
 500
 501 theorem lt_plus_minus:
 502  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus
 503 y (S x)))))))
 504 \def
 505  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(let TMP_1 \def (S
 506 x) in (le_plus_minus TMP_1 y H)))).
 507
 508 theorem lt_plus_minus_r:
 509  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y
 510 (S x)) x)))))
 511 \def
 512  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(let TMP_1 \def (S
 513 x) in (let TMP_2 \def (minus y TMP_1) in (let TMP_3 \def (plus x TMP_2) in
 514 (let TMP_5 \def (\lambda (n: nat).(let TMP_4 \def (S n) in (eq nat y TMP_4)))
 515 in (let TMP_6 \def (lt_plus_minus x y H) in (let TMP_7 \def (S x) in (let
 516 TMP_8 \def (minus y TMP_7) in (let TMP_9 \def (plus TMP_8 x) in (let TMP_10
 517 \def (S x) in (let TMP_11 \def (minus y TMP_10) in (let TMP_12 \def (plus_sym
 518 TMP_11 x) in (eq_ind_r nat TMP_3 TMP_5 TMP_6 TMP_9 TMP_12)))))))))))))).
 519
 520 theorem minus_x_SO:
 521  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
 522 \def
 523  \lambda (x: nat).(\lambda (H: (lt O x)).(let TMP_1 \def (minus x O) in (let
 524 TMP_2 \def (\lambda (n: nat).(eq nat x n)) in (let TMP_3 \def (\lambda (n:
 525 nat).(eq nat x n)) in (let TMP_4 \def (refl_equal nat x) in (let TMP_5 \def
 526 (minus x O) in (let TMP_6 \def (minus_n_O x) in (let TMP_7 \def (eq_ind nat x
 527 TMP_3 TMP_4 TMP_5 TMP_6) in (let TMP_8 \def (S O) in (let TMP_9 \def (minus x
 528 TMP_8) in (let TMP_10 \def (S TMP_9) in (let TMP_11 \def (minus_x_Sy x O H)
 529 in (eq_ind nat TMP_1 TMP_2 TMP_7 TMP_10 TMP_11))))))))))))).
 530
 531 theorem le_x_pred_y:
 532  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
 533 \def
 534  \lambda (y: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (x: nat).((lt x
 535 n) \to (let TMP_1 \def (pred n) in (le x TMP_1))))) in (let TMP_11 \def
 536 (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def (match H with [le_n
 537 \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let TMP_7 \def (S x) in (let
 538 TMP_8 \def (\lambda (e: nat).(match e with [O \Rightarrow False | (S _)
 539 \Rightarrow True])) in (let H1 \def (eq_ind nat TMP_7 TMP_8 I O H0) in (let
 540 TMP_9 \def (le x O) in (False_ind TMP_9 H1)))))) | (le_S m H0) \Rightarrow
 541 (\lambda (H1: (eq nat (S m) O)).(let TMP_3 \def (S m) in (let TMP_4 \def
 542 (\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
 543 True])) in (let H2 \def (eq_ind nat TMP_3 TMP_4 I O H1) in (let TMP_5 \def
 544 ((le (S x) m) \to (le x O)) in (let TMP_6 \def (False_ind TMP_5 H2) in (TMP_6
 545 H0)))))))]) in (let TMP_10 \def (refl_equal nat O) in (H0 TMP_10))))) in (let
 546 TMP_12 \def (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt x n) \to
 547 (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S n))).(le_S_n x n
 548 H0))))) in (nat_ind TMP_2 TMP_11 TMP_12 y)))).
 549
 550 theorem lt_le_minus:
 551  \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
 552 \def
 553  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(let TMP_1 \def (S
 554 O) in (let TMP_2 \def (S O) in (let TMP_3 \def (plus TMP_2 x) in (let TMP_4
 555 \def (\lambda (n: nat).(le n y)) in (let TMP_5 \def (S O) in (let TMP_6 \def
 556 (plus x TMP_5) in (let TMP_7 \def (S O) in (let TMP_8 \def (plus_sym x TMP_7)
 557 in (let TMP_9 \def (eq_ind_r nat TMP_3 TMP_4 H TMP_6 TMP_8) in (le_minus x y
 558 TMP_1 TMP_9)))))))))))).
 559
 560 theorem lt_le_e:
 561  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P))
 562 \to ((((le d n) \to P)) \to P))))
 563 \def
 564  \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n
 565 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in
 566 (let TMP_1 \def (le d n) in (let TMP_2 \def (lt n d) in (or_ind TMP_1 TMP_2 P
 567 H0 H H1)))))))).
 568
 569 theorem lt_eq_e:
 570  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
 571 \to ((((eq nat x y) \to P)) \to ((le x y) \to P)))))
 572 \def
 573  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x
 574 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x
 575 y)).(let TMP_1 \def (lt x y) in (let TMP_2 \def (eq nat x y) in (let TMP_3
 576 \def (le_lt_or_eq x y H1) in (or_ind TMP_1 TMP_2 P H H0 TMP_3))))))))).
 577
 578 theorem lt_eq_gt_e:
 579  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
 580 \to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P)))))
 581 \def
 582  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x
 583 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x)
 584 \to P))).(let TMP_3 \def (\lambda (H2: (le y x)).(let TMP_2 \def (\lambda
 585 (H3: (eq nat y x)).(let TMP_1 \def (sym_eq nat y x H3) in (H0 TMP_1))) in
 586 (lt_eq_e y x P H1 TMP_2 H2))) in (lt_le_e x y P H TMP_3))))))).
 587
 588 theorem lt_gen_xS:
 589  \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2
 590 nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n))))))
 591 \def
 592  \lambda (x: nat).(let TMP_6 \def (\lambda (n: nat).(\forall (n0: nat).((lt n
 593 (S n0)) \to (let TMP_1 \def (eq nat n O) in (let TMP_3 \def (\lambda (m:
 594 nat).(let TMP_2 \def (S m) in (eq nat n TMP_2))) in (let TMP_4 \def (\lambda
 595 (m: nat).(lt m n0)) in (let TMP_5 \def (ex2 nat TMP_3 TMP_4) in (or TMP_1
 596 TMP_5)))))))) in (let TMP_13 \def (\lambda (n: nat).(\lambda (_: (lt O (S
 597 n))).(let TMP_7 \def (eq nat O O) in (let TMP_9 \def (\lambda (m: nat).(let
 598 TMP_8 \def (S m) in (eq nat O TMP_8))) in (let TMP_10 \def (\lambda (m:
 599 nat).(lt m n)) in (let TMP_11 \def (ex2 nat TMP_9 TMP_10) in (let TMP_12 \def
 600 (refl_equal nat O) in (or_introl TMP_7 TMP_11 TMP_12)))))))) in (let TMP_30
 601 \def (\lambda (n: nat).(\lambda (_: ((\forall (n0: nat).((lt n (S n0)) \to
 602 (or (eq nat n O) (ex2 nat (\lambda (m: nat).(eq nat n (S m))) (\lambda (m:
 603 nat).(lt m n0)))))))).(\lambda (n0: nat).(\lambda (H0: (lt (S n) (S
 604 n0))).(let TMP_14 \def (S n) in (let TMP_15 \def (eq nat TMP_14 O) in (let
 605 TMP_18 \def (\lambda (m: nat).(let TMP_16 \def (S n) in (let TMP_17 \def (S
 606 m) in (eq nat TMP_16 TMP_17)))) in (let TMP_19 \def (\lambda (m: nat).(lt m
 607 n0)) in (let TMP_20 \def (ex2 nat TMP_18 TMP_19) in (let TMP_23 \def (\lambda
 608 (m: nat).(let TMP_21 \def (S n) in (let TMP_22 \def (S m) in (eq nat TMP_21
 609 TMP_22)))) in (let TMP_24 \def (\lambda (m: nat).(lt m n0)) in (let TMP_25
 610 \def (S n) in (let TMP_26 \def (refl_equal nat TMP_25) in (let TMP_27 \def (S
 611 n) in (let TMP_28 \def (le_S_n TMP_27 n0 H0) in (let TMP_29 \def (ex_intro2
 612 nat TMP_23 TMP_24 n TMP_26 TMP_28) in (or_intror TMP_15 TMP_20
 613 TMP_29))))))))))))))))) in (nat_ind TMP_6 TMP_13 TMP_30 x)))).
 614
 615 theorem le_lt_false:
 616  \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P:
 617 Prop).P))))
 618 \def
 619  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt
 620 y x)).(\lambda (P: Prop).(let TMP_1 \def (le_not_lt x y H H0) in (False_ind P
 621 TMP_1)))))).
 622
 623 theorem lt_neq:
 624  \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
 625 \def
 626  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq
 627 nat x y)).(let TMP_1 \def (\lambda (n: nat).(lt n y)) in (let H1 \def (eq_ind
 628 nat x TMP_1 H y H0) in (lt_n_n y H1)))))).
 629
 630 theorem arith0:
 631  \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n)
 632 \to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2))))))
 633 \def
 634  \lambda (h2: nat).(\lambda (d2: nat).(\lambda (n: nat).(\lambda (H: (le
 635 (plus d2 h2) n)).(\lambda (h1: nat).(let TMP_1 \def (plus d2 h1) in (let
 636 TMP_2 \def (plus h2 TMP_1) in (let TMP_3 \def (minus TMP_2 h2) in (let TMP_6
 637 \def (\lambda (n0: nat).(let TMP_4 \def (plus n h1) in (let TMP_5 \def (minus
 638 TMP_4 h2) in (le n0 TMP_5)))) in (let TMP_7 \def (plus d2 h1) in (let TMP_8
 639 \def (plus h2 TMP_7) in (let TMP_9 \def (plus d2 h1) in (let TMP_10 \def
 640 (le_plus_l h2 TMP_9) in (let TMP_11 \def (plus n h1) in (let TMP_12 \def
 641 (plus h2 d2) in (let TMP_13 \def (plus TMP_12 h1) in (let TMP_15 \def
 642 (\lambda (n0: nat).(let TMP_14 \def (plus n h1) in (le n0 TMP_14))) in (let
 643 TMP_16 \def (plus d2 h2) in (let TMP_19 \def (\lambda (n0: nat).(let TMP_17
 644 \def (plus n0 h1) in (let TMP_18 \def (plus n h1) in (le TMP_17 TMP_18)))) in
 645 (let TMP_20 \def (plus d2 h2) in (let TMP_21 \def (plus TMP_20 h1) in (let
 646 TMP_22 \def (plus n h1) in (let TMP_23 \def (plus d2 h2) in (let TMP_24 \def
 647 (plus TMP_23 h1) in (let TMP_25 \def (plus n h1) in (let TMP_26 \def (plus d2
 648 h2) in (let TMP_27 \def (le_n h1) in (let TMP_28 \def (le_plus_plus TMP_26 n
 649 h1 h1 H TMP_27) in (let TMP_29 \def (le_n_S TMP_24 TMP_25 TMP_28) in (let
 650 TMP_30 \def (le_S_n TMP_21 TMP_22 TMP_29) in (let TMP_31 \def (plus h2 d2) in
 651 (let TMP_32 \def (plus_sym h2 d2) in (let TMP_33 \def (eq_ind_r nat TMP_16
 652 TMP_19 TMP_30 TMP_31 TMP_32) in (let TMP_34 \def (plus d2 h1) in (let TMP_35
 653 \def (plus h2 TMP_34) in (let TMP_36 \def (plus_assoc_l h2 d2 h1) in (let
 654 TMP_37 \def (eq_ind_r nat TMP_13 TMP_15 TMP_33 TMP_35 TMP_36) in (let TMP_38
 655 \def (le_minus_minus h2 TMP_8 TMP_10 TMP_11 TMP_37) in (let TMP_39 \def (plus
 656 d2 h1) in (let TMP_40 \def (plus d2 h1) in (let TMP_41 \def (minus_plus h2
 657 TMP_40) in (eq_ind nat TMP_3 TMP_6 TMP_38 TMP_39
 658 TMP_41))))))))))))))))))))))))))))))))))))))))).
 659
 660 theorem O_minus:
 661  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
 662 \def
 663  \lambda (x: nat).(let TMP_2 \def (\lambda (n: nat).(\forall (y: nat).((le n
 664 y) \to (let TMP_1 \def (minus n y) in (eq nat TMP_1 O))))) in (let TMP_3 \def
 665 (\lambda (y: nat).(\lambda (_: (le O y)).(refl_equal nat O))) in (let TMP_20
 666 \def (\lambda (x0: nat).(\lambda (H: ((\forall (y: nat).((le x0 y) \to (eq
 667 nat (minus x0 y) O))))).(\lambda (y: nat).(let TMP_5 \def (\lambda (n:
 668 nat).((le (S x0) n) \to (let TMP_4 \def (match n with [O \Rightarrow (S x0) |
 669 (S l) \Rightarrow (minus x0 l)]) in (eq nat TMP_4 O)))) in (let TMP_17 \def
 670 (\lambda (H0: (le (S x0) O)).(let TMP_7 \def (\lambda (n: nat).(let TMP_6
 671 \def (S n) in (eq nat O TMP_6))) in (let TMP_8 \def (\lambda (n: nat).(le x0
 672 n)) in (let TMP_9 \def (S x0) in (let TMP_10 \def (eq nat TMP_9 O) in (let
 673 TMP_15 \def (\lambda (x1: nat).(\lambda (H1: (eq nat O (S x1))).(\lambda (_:
 674 (le x0 x1)).(let TMP_11 \def (\lambda (ee: nat).(match ee with [O \Rightarrow
 675 True | (S _) \Rightarrow False])) in (let TMP_12 \def (S x1) in (let H3 \def
 676 (eq_ind nat O TMP_11 I TMP_12 H1) in (let TMP_13 \def (S x0) in (let TMP_14
 677 \def (eq nat TMP_13 O) in (False_ind TMP_14 H3))))))))) in (let TMP_16 \def
 678 (le_gen_S x0 O H0) in (ex2_ind nat TMP_7 TMP_8 TMP_10 TMP_15 TMP_16))))))))
 679 in (let TMP_19 \def (\lambda (n: nat).(\lambda (_: (((le (S x0) n) \to (eq
 680 nat (match n with [O \Rightarrow (S x0) | (S l) \Rightarrow (minus x0 l)])
 681 O)))).(\lambda (H1: (le (S x0) (S n))).(let TMP_18 \def (le_S_n x0 n H1) in
 682 (H n TMP_18))))) in (nat_ind TMP_5 TMP_17 TMP_19 y))))))) in (nat_ind TMP_2
 683 TMP_3 TMP_20 x)))).
 684
 685 theorem minus_minus:
 686  \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y)
 687 \to ((eq nat (minus x z) (minus y z)) \to (eq nat x y))))))
 688 \def
 689  \lambda (z: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (x:
 690 nat).(\forall (y: nat).((le n x) \to ((le n y) \to ((eq nat (minus x n)
 691 (minus y n)) \to (eq nat x y))))))) in (let TMP_9 \def (\lambda (x:
 692 nat).(\lambda (y: nat).(\lambda (_: (le O x)).(\lambda (_: (le O y)).(\lambda
 693 (H1: (eq nat (minus x O) (minus y O))).(let TMP_2 \def (minus x O) in (let
 694 TMP_4 \def (\lambda (n: nat).(let TMP_3 \def (minus y O) in (eq nat n
 695 TMP_3))) in (let TMP_5 \def (minus_n_O x) in (let H2 \def (eq_ind_r nat TMP_2
 696 TMP_4 H1 x TMP_5) in (let TMP_6 \def (minus y O) in (let TMP_7 \def (\lambda
 697 (n: nat).(eq nat x n)) in (let TMP_8 \def (minus_n_O y) in (let H3 \def
 698 (eq_ind_r nat TMP_6 TMP_7 H2 y TMP_8) in H3))))))))))))) in (let TMP_40 \def
 699 (\lambda (z0: nat).(\lambda (IH: ((\forall (x: nat).(\forall (y: nat).((le z0
 700 x) \to ((le z0 y) \to ((eq nat (minus x z0) (minus y z0)) \to (eq nat x
 701 y)))))))).(\lambda (x: nat).(let TMP_10 \def (\lambda (n: nat).(\forall (y:
 702 nat).((le (S z0) n) \to ((le (S z0) y) \to ((eq nat (minus n (S z0)) (minus y
 703 (S z0))) \to (eq nat n y)))))) in (let TMP_20 \def (\lambda (y: nat).(\lambda
 704 (H: (le (S z0) O)).(\lambda (_: (le (S z0) y)).(\lambda (_: (eq nat (minus O
 705 (S z0)) (minus y (S z0)))).(let TMP_12 \def (\lambda (n: nat).(let TMP_11
 706 \def (S n) in (eq nat O TMP_11))) in (let TMP_13 \def (\lambda (n: nat).(le
 707 z0 n)) in (let TMP_14 \def (eq nat O y) in (let TMP_18 \def (\lambda (x0:
 708 nat).(\lambda (H2: (eq nat O (S x0))).(\lambda (_: (le z0 x0)).(let TMP_15
 709 \def (\lambda (ee: nat).(match ee with [O \Rightarrow True | (S _)
 710 \Rightarrow False])) in (let TMP_16 \def (S x0) in (let H4 \def (eq_ind nat O
 711 TMP_15 I TMP_16 H2) in (let TMP_17 \def (eq nat O y) in (False_ind TMP_17
 712 H4)))))))) in (let TMP_19 \def (le_gen_S z0 O H) in (ex2_ind nat TMP_12
 713 TMP_13 TMP_14 TMP_18 TMP_19)))))))))) in (let TMP_39 \def (\lambda (x0:
 714 nat).(\lambda (_: ((\forall (y: nat).((le (S z0) x0) \to ((le (S z0) y) \to
 715 ((eq nat (minus x0 (S z0)) (minus y (S z0))) \to (eq nat x0 y))))))).(\lambda
 716 (y: nat).(let TMP_22 \def (\lambda (n: nat).((le (S z0) (S x0)) \to ((le (S
 717 z0) n) \to ((eq nat (minus (S x0) (S z0)) (minus n (S z0))) \to (let TMP_21
 718 \def (S x0) in (eq nat TMP_21 n)))))) in (let TMP_34 \def (\lambda (H: (le (S
 719 z0) (S x0))).(\lambda (H0: (le (S z0) O)).(\lambda (_: (eq nat (minus (S x0)
 720 (S z0)) (minus O (S z0)))).(let H_y \def (le_S_n z0 x0 H) in (let TMP_24 \def
 721 (\lambda (n: nat).(let TMP_23 \def (S n) in (eq nat O TMP_23))) in (let
 722 TMP_25 \def (\lambda (n: nat).(le z0 n)) in (let TMP_26 \def (S x0) in (let
 723 TMP_27 \def (eq nat TMP_26 O) in (let TMP_32 \def (\lambda (x1: nat).(\lambda
 724 (H2: (eq nat O (S x1))).(\lambda (_: (le z0 x1)).(let TMP_28 \def (\lambda
 725 (ee: nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) in
 726 (let TMP_29 \def (S x1) in (let H4 \def (eq_ind nat O TMP_28 I TMP_29 H2) in
 727 (let TMP_30 \def (S x0) in (let TMP_31 \def (eq nat TMP_30 O) in (False_ind
 728 TMP_31 H4))))))))) in (let TMP_33 \def (le_gen_S z0 O H0) in (ex2_ind nat
 729 TMP_24 TMP_25 TMP_27 TMP_32 TMP_33))))))))))) in (let TMP_38 \def (\lambda
 730 (y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to ((eq nat
 731 (minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0) y0)))))).(\lambda
 732 (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S y0))).(\lambda (H1: (eq
 733 nat (minus (S x0) (S z0)) (minus (S y0) (S z0)))).(let TMP_35 \def (le_S_n z0
 734 x0 H) in (let TMP_36 \def (le_S_n z0 y0 H0) in (let TMP_37 \def (IH x0 y0
 735 TMP_35 TMP_36 H1) in (f_equal nat nat S x0 y0 TMP_37))))))))) in (nat_ind
 736 TMP_22 TMP_34 TMP_38 y))))))) in (nat_ind TMP_10 TMP_20 TMP_39 x))))))) in
 737 (nat_ind TMP_1 TMP_9 TMP_40 z)))).
 738
 739 theorem plus_plus:
 740  \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1:
 741 nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z
 742 x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1)))))))))
 743 \def
 744  \lambda (z: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (x1:
 745 nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 n) \to
 746 ((le x2 n) \to ((eq nat (plus (minus n x1) y1) (plus (minus n x2) y2)) \to
 747 (let TMP_1 \def (plus x1 y2) in (let TMP_2 \def (plus x2 y1) in (eq nat TMP_1
 748 TMP_2))))))))))) in (let TMP_17 \def (\lambda (x1: nat).(\lambda (x2:
 749 nat).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le x1 O)).(\lambda
 750 (H0: (le x2 O)).(\lambda (H1: (eq nat y1 y2)).(let TMP_6 \def (\lambda (n:
 751 nat).(let TMP_4 \def (plus x1 n) in (let TMP_5 \def (plus x2 y1) in (eq nat
 752 TMP_4 TMP_5)))) in (let H_y \def (le_n_O_eq x2 H0) in (let TMP_9 \def
 753 (\lambda (n: nat).(let TMP_7 \def (plus x1 y1) in (let TMP_8 \def (plus n y1)
 754 in (eq nat TMP_7 TMP_8)))) in (let H_y0 \def (le_n_O_eq x1 H) in (let TMP_12
 755 \def (\lambda (n: nat).(let TMP_10 \def (plus n y1) in (let TMP_11 \def (plus
 756 O y1) in (eq nat TMP_10 TMP_11)))) in (let TMP_13 \def (plus O y1) in (let
 757 TMP_14 \def (refl_equal nat TMP_13) in (let TMP_15 \def (eq_ind nat O TMP_12
 758 TMP_14 x1 H_y0) in (let TMP_16 \def (eq_ind nat O TMP_9 TMP_15 x2 H_y) in
 759 (eq_ind nat y1 TMP_6 TMP_16 y2 H1))))))))))))))))) in (let TMP_91 \def
 760 (\lambda (z0: nat).(\lambda (IH: ((\forall (x1: nat).(\forall (x2:
 761 nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z0) \to ((le x2 z0) \to
 762 ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2)) \to (eq nat (plus
 763 x1 y2) (plus x2 y1))))))))))).(\lambda (x1: nat).(let TMP_20 \def (\lambda
 764 (n: nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le n (S
 765 z0)) \to ((le x2 (S z0)) \to ((eq nat (plus (minus (S z0) n) y1) (plus (minus
 766 (S z0) x2) y2)) \to (let TMP_18 \def (plus n y2) in (let TMP_19 \def (plus x2
 767 y1) in (eq nat TMP_18 TMP_19)))))))))) in (let TMP_56 \def (\lambda (x2:
 768 nat).(let TMP_23 \def (\lambda (n: nat).(\forall (y1: nat).(\forall (y2:
 769 nat).((le O (S z0)) \to ((le n (S z0)) \to ((eq nat (plus (minus (S z0) O)
 770 y1) (plus (minus (S z0) n) y2)) \to (let TMP_21 \def (plus O y2) in (let
 771 TMP_22 \def (plus n y1) in (eq nat TMP_21 TMP_22))))))))) in (let TMP_32 \def
 772 (\lambda (y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda
 773 (_: (le O (S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (S (plus z0
 774 y2)))).(let H_y \def (IH O O) in (let TMP_24 \def (minus z0 O) in (let TMP_25
 775 \def (\lambda (n: nat).(\forall (y3: nat).(\forall (y4: nat).((le O z0) \to
 776 ((le O z0) \to ((eq nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) in
 777 (let TMP_26 \def (minus_n_O z0) in (let H2 \def (eq_ind_r nat TMP_24 TMP_25
 778 H_y z0 TMP_26) in (let TMP_27 \def (le_O_n z0) in (let TMP_28 \def (le_O_n
 779 z0) in (let TMP_29 \def (plus z0 y1) in (let TMP_30 \def (plus z0 y2) in (let
 780 TMP_31 \def (eq_add_S TMP_29 TMP_30 H1) in (H2 y1 y2 TMP_27 TMP_28
 781 TMP_31)))))))))))))))) in (let TMP_55 \def (\lambda (x3: nat).(\lambda (_:
 782 ((\forall (y1: nat).(\forall (y2: nat).((le O (S z0)) \to ((le x3 (S z0)) \to
 783 ((eq nat (S (plus z0 y1)) (plus (match x3 with [O \Rightarrow (S z0) | (S l)
 784 \Rightarrow (minus z0 l)]) y2)) \to (eq nat y2 (plus x3 y1))))))))).(\lambda
 785 (y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S
 786 x3) (S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3)
 787 y2))).(let TMP_33 \def (S y1) in (let H_y \def (IH O x3 TMP_33) in (let
 788 TMP_34 \def (minus z0 O) in (let TMP_37 \def (\lambda (n: nat).(\forall (y3:
 789 nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S y1)) (plus (minus z0
 790 x3) y3)) \to (let TMP_35 \def (S y1) in (let TMP_36 \def (plus x3 TMP_35) in
 791 (eq nat y3 TMP_36)))))))) in (let TMP_38 \def (minus_n_O z0) in (let H2 \def
 792 (eq_ind_r nat TMP_34 TMP_37 H_y z0 TMP_38) in (let TMP_39 \def (S y1) in (let
 793 TMP_40 \def (plus z0 TMP_39) in (let TMP_43 \def (\lambda (n: nat).(\forall
 794 (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus (minus z0 x3) y3))
 795 \to (let TMP_41 \def (S y1) in (let TMP_42 \def (plus x3 TMP_41) in (eq nat
 796 y3 TMP_42)))))))) in (let TMP_44 \def (plus z0 y1) in (let TMP_45 \def (S
 797 TMP_44) in (let TMP_46 \def (plus_n_Sm z0 y1) in (let H3 \def (eq_ind_r nat
 798 TMP_40 TMP_43 H2 TMP_45 TMP_46) in (let TMP_47 \def (S y1) in (let TMP_48
 799 \def (plus x3 TMP_47) in (let TMP_49 \def (\lambda (n: nat).(\forall (y3:
 800 nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus z0 y1)) (plus (minus z0
 801 x3) y3)) \to (eq nat y3 n)))))) in (let TMP_50 \def (plus x3 y1) in (let
 802 TMP_51 \def (S TMP_50) in (let TMP_52 \def (plus_n_Sm x3 y1) in (let H4 \def
 803 (eq_ind_r nat TMP_48 TMP_49 H3 TMP_51 TMP_52) in (let TMP_53 \def (le_O_n z0)
 804 in (let TMP_54 \def (le_S_n x3 z0 H0) in (H4 y2 TMP_53 TMP_54
 805 H1)))))))))))))))))))))))))))))) in (nat_ind TMP_23 TMP_32 TMP_55 x2))))) in
 806 (let TMP_90 \def (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall
 807 (y1: nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat
 808 (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2
 809 y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(let TMP_60 \def (\lambda (n:
 810 nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S
 811 z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2))
 812 \to (let TMP_57 \def (S x2) in (let TMP_58 \def (plus TMP_57 y2) in (let
 813 TMP_59 \def (plus n y1) in (eq nat TMP_58 TMP_59)))))))))) in (let TMP_83
 814 \def (\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S
 815 z0))).(\lambda (_: (le O (S z0))).(\lambda (H1: (eq nat (plus (minus z0 x2)
 816 y1) (S (plus z0 y2)))).(let TMP_61 \def (S y2) in (let H_y \def (IH x2 O y1
 817 TMP_61) in (let TMP_62 \def (minus z0 O) in (let TMP_65 \def (\lambda (n:
 818 nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) (plus n
 819 (S y2))) \to (let TMP_63 \def (S y2) in (let TMP_64 \def (plus x2 TMP_63) in
 820 (eq nat TMP_64 y1))))))) in (let TMP_66 \def (minus_n_O z0) in (let H2 \def
 821 (eq_ind_r nat TMP_62 TMP_65 H_y z0 TMP_66) in (let TMP_67 \def (S y2) in (let
 822 TMP_68 \def (plus z0 TMP_67) in (let TMP_71 \def (\lambda (n: nat).((le x2
 823 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (let TMP_69
 824 \def (S y2) in (let TMP_70 \def (plus x2 TMP_69) in (eq nat TMP_70 y1)))))))
 825 in (let TMP_72 \def (plus z0 y2) in (let TMP_73 \def (S TMP_72) in (let
 826 TMP_74 \def (plus_n_Sm z0 y2) in (let H3 \def (eq_ind_r nat TMP_68 TMP_71 H2
 827 TMP_73 TMP_74) in (let TMP_75 \def (S y2) in (let TMP_76 \def (plus x2
 828 TMP_75) in (let TMP_77 \def (\lambda (n: nat).((le x2 z0) \to ((le O z0) \to
 829 ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1))))) in
 830 (let TMP_78 \def (plus x2 y2) in (let TMP_79 \def (S TMP_78) in (let TMP_80
 831 \def (plus_n_Sm x2 y2) in (let H4 \def (eq_ind_r nat TMP_76 TMP_77 H3 TMP_79
 832 TMP_80) in (let TMP_81 \def (le_S_n x2 z0 H) in (let TMP_82 \def (le_O_n z0)
 833 in (H4 TMP_81 TMP_82 H1)))))))))))))))))))))))))))) in (let TMP_89 \def
 834 (\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2: nat).((le
 835 (S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus z0 x2) y1) (plus
 836 (match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2))
 837 \to (eq nat (S (plus x2 y2)) (plus x4 y1))))))))).(\lambda (y1: nat).(\lambda
 838 (y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (H0: (le (S x4) (S
 839 z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4)
 840 y2))).(let TMP_84 \def (plus x2 y2) in (let TMP_85 \def (plus x4 y1) in (let
 841 TMP_86 \def (le_S_n x2 z0 H) in (let TMP_87 \def (le_S_n x4 z0 H0) in (let
 842 TMP_88 \def (IH x2 x4 y1 y2 TMP_86 TMP_87 H1) in (f_equal nat nat S TMP_84
 843 TMP_85 TMP_88))))))))))))) in (nat_ind TMP_60 TMP_83 TMP_89 x3))))))) in
 844 (nat_ind TMP_20 TMP_56 TMP_90 x1))))))) in (nat_ind TMP_3 TMP_17 TMP_91 z)))).
 845
 846 theorem le_S_minus:
 847  \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to
 848 (le d (S (minus n h))))))
 849 \def
 850  \lambda (d: nat).(\lambda (h: nat).(\lambda (n: nat).(\lambda (H: (le (plus
 851 d h) n)).(let TMP_1 \def (plus d h) in (let TMP_2 \def (le_plus_l d h) in
 852 (let H0 \def (le_trans d TMP_1 n TMP_2 H) in (let TMP_3 \def (\lambda (n0:
 853 nat).(le d n0)) in (let TMP_4 \def (minus n h) in (let TMP_5 \def (plus TMP_4
 854 h) in (let TMP_6 \def (plus d h) in (let TMP_7 \def (le_plus_r d h) in (let
 855 TMP_8 \def (le_trans h TMP_6 n TMP_7 H) in (let TMP_9 \def (le_plus_minus_sym
 856 h n TMP_8) in (let H1 \def (eq_ind nat n TMP_3 H0 TMP_5 TMP_9) in (let TMP_10
 857 \def (minus n h) in (let TMP_11 \def (le_minus d n h H) in (le_S d TMP_10
 858 TMP_11))))))))))))))))).
 859
 860 theorem lt_x_pred_y:
 861  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
 862 \def
 863  \lambda (x: nat).(\lambda (y: nat).(let TMP_2 \def (\lambda (n: nat).((lt x
 864 (pred n)) \to (let TMP_1 \def (S x) in (lt TMP_1 n)))) in (let TMP_5 \def
 865 (\lambda (H: (lt x O)).(let TMP_3 \def (S x) in (let TMP_4 \def (lt TMP_3 O)
 866 in (lt_x_O x H TMP_4)))) in (let TMP_6 \def (\lambda (n: nat).(\lambda (_:
 867 (((lt x (pred n)) \to (lt (S x) n)))).(\lambda (H0: (lt x n)).(lt_n_S x n
 868 H0)))) in (nat_ind TMP_2 TMP_5 TMP_6 y))))).
 869