matita/matita/contribs/lambdadelta/legacy_1/coq/props.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 "legacy_1/coq/fwd.ma".
  18
  19 theorem f_equal:
  20  \forall (A: Type[0]).(\forall (B: Type[0]).(\forall (f: ((A \to
  21 B))).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
  22 \def
  23  \lambda (A: Type[0]).(\lambda (B: Type[0]).(\lambda (f: ((A \to
  24 B))).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x y)).(let TMP_3 \def
  25 (\lambda (a: A).(let TMP_1 \def (f x) in (let TMP_2 \def (f a) in (eq B TMP_1
  26 TMP_2)))) in (let TMP_4 \def (f x) in (let TMP_5 \def (refl_equal B TMP_4) in
  27 (eq_ind A x TMP_3 TMP_5 y H))))))))).
  28
  29 theorem f_equal2:
  30  \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (B: Type[0]).(\forall
  31 (f: ((A1 \to (A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2:
  32 A2).(\forall (y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2)
  33 (f y1 y2)))))))))))
  34 \def
  35  \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (B: Type[0]).(\lambda
  36 (f: ((A1 \to (A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2:
  37 A2).(\lambda (y2: A2).(\lambda (H: (eq A1 x1 y1)).(let TMP_3 \def (\lambda
  38 (a: A1).((eq A2 x2 y2) \to (let TMP_1 \def (f x1 x2) in (let TMP_2 \def (f a
  39 y2) in (eq B TMP_1 TMP_2))))) in (let TMP_9 \def (\lambda (H0: (eq A2 x2
  40 y2)).(let TMP_6 \def (\lambda (a: A2).(let TMP_4 \def (f x1 x2) in (let TMP_5
  41 \def (f x1 a) in (eq B TMP_4 TMP_5)))) in (let TMP_7 \def (f x1 x2) in (let
  42 TMP_8 \def (refl_equal B TMP_7) in (eq_ind A2 x2 TMP_6 TMP_8 y2 H0))))) in
  43 (eq_ind A1 x1 TMP_3 TMP_9 y1 H))))))))))).
  44
  45 theorem f_equal3:
  46  \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (A3: Type[0]).(\forall
  47 (B: Type[0]).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1:
  48 A1).(\forall (y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3:
  49 A3).(\forall (y3: A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3)
  50 \to (eq B (f x1 x2 x3) (f y1 y2 y3)))))))))))))))
  51 \def
  52  \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (A3: Type[0]).(\lambda
  53 (B: Type[0]).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1:
  54 A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3:
  55 A3).(\lambda (y3: A3).(\lambda (H: (eq A1 x1 y1)).(let TMP_3 \def (\lambda
  56 (a: A1).((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (let TMP_1 \def (f x1 x2 x3) in
  57 (let TMP_2 \def (f a y2 y3) in (eq B TMP_1 TMP_2)))))) in (let TMP_13 \def
  58 (\lambda (H0: (eq A2 x2 y2)).(let TMP_6 \def (\lambda (a: A2).((eq A3 x3 y3)
  59 \to (let TMP_4 \def (f x1 x2 x3) in (let TMP_5 \def (f x1 a y3) in (eq B
  60 TMP_4 TMP_5))))) in (let TMP_12 \def (\lambda (H1: (eq A3 x3 y3)).(let TMP_9
  61 \def (\lambda (a: A3).(let TMP_7 \def (f x1 x2 x3) in (let TMP_8 \def (f x1
  62 x2 a) in (eq B TMP_7 TMP_8)))) in (let TMP_10 \def (f x1 x2 x3) in (let
  63 TMP_11 \def (refl_equal B TMP_10) in (eq_ind A3 x3 TMP_9 TMP_11 y3 H1))))) in
  64 (eq_ind A2 x2 TMP_6 TMP_12 y2 H0)))) in (eq_ind A1 x1 TMP_3 TMP_13 y1
  65 H)))))))))))))).
  66
  67 theorem sym_eq:
  68  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y
  69 x))))
  70 \def
  71  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
  72 y)).(let TMP_1 \def (\lambda (a: A).(eq A a x)) in (let TMP_2 \def
  73 (refl_equal A x) in (eq_ind A x TMP_1 TMP_2 y H)))))).
  74
  75 theorem eq_ind_r:
  76  \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
  77 (\forall (y: A).((eq A y x) \to (P y))))))
  78 \def
  79  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda
  80 (H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0)
  81 with [refl_equal \Rightarrow H])))))).
  82
  83 theorem trans_eq:
  84  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A
  85 x y) \to ((eq A y z) \to (eq A x z))))))
  86 \def
  87  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (z:
  88 A).(\lambda (H: (eq A x y)).(\lambda (H0: (eq A y z)).(let TMP_1 \def
  89 (\lambda (a: A).(eq A x a)) in (eq_ind A y TMP_1 H z H0))))))).
  90
  91 theorem sym_not_eq:
  92  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to
  93 (not (eq A y x)))))
  94 \def
  95  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq
  96 A x y))).(\lambda (h2: (eq A y x)).(let TMP_1 \def (\lambda (a: A).(eq A a
  97 y)) in (let TMP_2 \def (refl_equal A y) in (let TMP_3 \def (eq_ind A y TMP_1
  98 TMP_2 x h2) in (h1 TMP_3)))))))).
  99
 100 theorem nat_double_ind:
 101  \forall (R: ((nat \to (nat \to Prop)))).(((\forall (n: nat).(R O n))) \to
 102 (((\forall (n: nat).(R (S n) O))) \to (((\forall (n: nat).(\forall (m:
 103 nat).((R n m) \to (R (S n) (S m)))))) \to (\forall (n: nat).(\forall (m:
 104 nat).(R n m))))))
 105 \def
 106  \lambda (R: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (n: nat).(R O
 107 n)))).(\lambda (H0: ((\forall (n: nat).(R (S n) O)))).(\lambda (H1: ((\forall
 108 (n: nat).(\forall (m: nat).((R n m) \to (R (S n) (S m))))))).(\lambda (n:
 109 nat).(let TMP_1 \def (\lambda (n0: nat).(\forall (m: nat).(R n0 m))) in (let
 110 TMP_7 \def (\lambda (n0: nat).(\lambda (H2: ((\forall (m: nat).(R n0
 111 m)))).(\lambda (m: nat).(let TMP_3 \def (\lambda (n1: nat).(let TMP_2 \def (S
 112 n0) in (R TMP_2 n1))) in (let TMP_4 \def (H0 n0) in (let TMP_6 \def (\lambda
 113 (n1: nat).(\lambda (_: (R (S n0) n1)).(let TMP_5 \def (H2 n1) in (H1 n0 n1
 114 TMP_5)))) in (nat_ind TMP_3 TMP_4 TMP_6 m))))))) in (nat_ind TMP_1 H TMP_7
 115 n))))))).
 116
 117 theorem eq_add_S:
 118  \forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
 119 \def
 120  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S m))).(let
 121 TMP_1 \def (S n) in (let TMP_2 \def (S m) in (f_equal nat nat pred TMP_1
 122 TMP_2 H))))).
 123
 124 theorem O_S:
 125  \forall (n: nat).(not (eq nat O (S n)))
 126 \def
 127  \lambda (n: nat).(\lambda (H: (eq nat O (S n))).(let TMP_1 \def (S n) in
 128 (let TMP_2 \def (\lambda (n0: nat).(IsSucc n0)) in (let TMP_3 \def (S n) in
 129 (let TMP_4 \def (sym_eq nat O TMP_3 H) in (eq_ind nat TMP_1 TMP_2 I O
 130 TMP_4)))))).
 131
 132 theorem not_eq_S:
 133  \forall (n: nat).(\forall (m: nat).((not (eq nat n m)) \to (not (eq nat (S
 134 n) (S m)))))
 135 \def
 136  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda
 137 (H0: (eq nat (S n) (S m))).(let TMP_1 \def (eq_add_S n m H0) in (H TMP_1))))).
 138
 139 theorem pred_Sn:
 140  \forall (m: nat).(eq nat m (pred (S m)))
 141 \def
 142  \lambda (m: nat).(let TMP_1 \def (S m) in (let TMP_2 \def (pred TMP_1) in
 143 (refl_equal nat TMP_2))).
 144
 145 theorem S_pred:
 146  \forall (n: nat).(\forall (m: nat).((lt m n) \to (eq nat n (S (pred n)))))
 147 \def
 148  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt m n)).(let TMP_1 \def (S
 149 m) in (let TMP_4 \def (\lambda (n0: nat).(let TMP_2 \def (pred n0) in (let
 150 TMP_3 \def (S TMP_2) in (eq nat n0 TMP_3)))) in (let TMP_5 \def (S m) in (let
 151 TMP_6 \def (pred TMP_5) in (let TMP_7 \def (S TMP_6) in (let TMP_8 \def
 152 (refl_equal nat TMP_7) in (let TMP_12 \def (\lambda (m0: nat).(\lambda (_:
 153 (le (S m) m0)).(\lambda (_: (eq nat m0 (S (pred m0)))).(let TMP_9 \def (S m0)
 154 in (let TMP_10 \def (pred TMP_9) in (let TMP_11 \def (S TMP_10) in
 155 (refl_equal nat TMP_11))))))) in (le_ind TMP_1 TMP_4 TMP_8 TMP_12 n
 156 H)))))))))).
 157
 158 theorem le_trans:
 159  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((le m p)
 160 \to (le n p)))))
 161 \def
 162  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 163 m)).(\lambda (H0: (le m p)).(let TMP_1 \def (\lambda (n0: nat).(le n n0)) in
 164 (let TMP_2 \def (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle:
 165 (le n m0)).(le_S n m0 IHle)))) in (le_ind m TMP_1 H TMP_2 p H0))))))).
 166
 167 theorem le_trans_S:
 168  \forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
 169 \def
 170  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(let TMP_1
 171 \def (S n) in (let TMP_2 \def (le_n n) in (let TMP_3 \def (le_S n n TMP_2) in
 172 (le_trans n TMP_1 m TMP_3 H)))))).
 173
 174 theorem le_n_S:
 175  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
 176 \def
 177  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(let TMP_3 \def
 178 (\lambda (n0: nat).(let TMP_1 \def (S n) in (let TMP_2 \def (S n0) in (le
 179 TMP_1 TMP_2)))) in (let TMP_4 \def (S n) in (let TMP_5 \def (le_n TMP_4) in
 180 (let TMP_8 \def (\lambda (m0: nat).(\lambda (_: (le n m0)).(\lambda (IHle:
 181 (le (S n) (S m0))).(let TMP_6 \def (S n) in (let TMP_7 \def (S m0) in (le_S
 182 TMP_6 TMP_7 IHle)))))) in (le_ind n TMP_3 TMP_5 TMP_8 m H))))))).
 183
 184 theorem le_O_n:
 185  \forall (n: nat).(le O n)
 186 \def
 187  \lambda (n: nat).(let TMP_1 \def (\lambda (n0: nat).(le O n0)) in (let TMP_2
 188 \def (le_n O) in (let TMP_3 \def (\lambda (n0: nat).(\lambda (IHn: (le O
 189 n0)).(le_S O n0 IHn))) in (nat_ind TMP_1 TMP_2 TMP_3 n)))).
 190
 191 theorem le_S_n:
 192  \forall (n: nat).(\forall (m: nat).((le (S n) (S m)) \to (le n m)))
 193 \def
 194  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) (S m))).(let TMP_1
 195 \def (S n) in (let TMP_5 \def (\lambda (n0: nat).(let TMP_2 \def (S n) in
 196 (let TMP_3 \def (pred TMP_2) in (let TMP_4 \def (pred n0) in (le TMP_3
 197 TMP_4))))) in (let TMP_6 \def (le_n n) in (let TMP_7 \def (\lambda (m0:
 198 nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S
 199 n m0 H0)))) in (let TMP_8 \def (S m) in (le_ind TMP_1 TMP_5 TMP_6 TMP_7 TMP_8
 200 H)))))))).
 201
 202 theorem le_Sn_O:
 203  \forall (n: nat).(not (le (S n) O))
 204 \def
 205  \lambda (n: nat).(\lambda (H: (le (S n) O)).(let TMP_1 \def (S n) in (let
 206 TMP_2 \def (\lambda (n0: nat).(IsSucc n0)) in (let TMP_3 \def (\lambda (m:
 207 nat).(\lambda (_: (le (S n) m)).(\lambda (_: (IsSucc m)).I))) in (le_ind
 208 TMP_1 TMP_2 I TMP_3 O H))))).
 209
 210 theorem le_Sn_n:
 211  \forall (n: nat).(not (le (S n) n))
 212 \def
 213  \lambda (n: nat).(let TMP_3 \def (\lambda (n0: nat).(let TMP_1 \def (S n0)
 214 in (let TMP_2 \def (le TMP_1 n0) in (not TMP_2)))) in (let TMP_4 \def
 215 (le_Sn_O O) in (let TMP_7 \def (\lambda (n0: nat).(\lambda (IHn: (not (le (S
 216 n0) n0))).(\lambda (H: (le (S (S n0)) (S n0))).(let TMP_5 \def (S n0) in (let
 217 TMP_6 \def (le_S_n TMP_5 n0 H) in (IHn TMP_6)))))) in (nat_ind TMP_3 TMP_4
 218 TMP_7 n)))).
 219
 220 theorem le_antisym:
 221  \forall (n: nat).(\forall (m: nat).((le n m) \to ((le m n) \to (eq nat n
 222 m))))
 223 \def
 224  \lambda (n: nat).(\lambda (m: nat).(\lambda (h: (le n m)).(let TMP_1 \def
 225 (\lambda (n0: nat).((le n0 n) \to (eq nat n n0))) in (let TMP_2 \def (\lambda
 226 (_: (le n n)).(refl_equal nat n)) in (let TMP_8 \def (\lambda (m0:
 227 nat).(\lambda (H: (le n m0)).(\lambda (_: (((le m0 n) \to (eq nat n
 228 m0)))).(\lambda (H1: (le (S m0) n)).(let TMP_3 \def (S m0) in (let TMP_4 \def
 229 (eq nat n TMP_3) in (let TMP_5 \def (S m0) in (let H2 \def (le_trans TMP_5 n
 230 m0 H1 H) in (let H3 \def (le_Sn_n m0) in (let TMP_6 \def (\lambda (H4: (le (S
 231 m0) m0)).(H3 H4)) in (let TMP_7 \def (TMP_6 H2) in (False_ind TMP_4
 232 TMP_7)))))))))))) in (le_ind n TMP_1 TMP_2 TMP_8 m h)))))).
 233
 234 theorem le_n_O_eq:
 235  \forall (n: nat).((le n O) \to (eq nat O n))
 236 \def
 237  \lambda (n: nat).(\lambda (H: (le n O)).(let TMP_1 \def (le_O_n n) in
 238 (le_antisym O n TMP_1 H))).
 239
 240 theorem le_elim_rel:
 241  \forall (P: ((nat \to (nat \to Prop)))).(((\forall (p: nat).(P O p))) \to
 242 (((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p q) \to (P (S p) (S
 243 q))))))) \to (\forall (n: nat).(\forall (m: nat).((le n m) \to (P n m))))))
 244 \def
 245  \lambda (P: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (p: nat).(P O
 246 p)))).(\lambda (H0: ((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p
 247 q) \to (P (S p) (S q)))))))).(\lambda (n: nat).(let TMP_1 \def (\lambda (n0:
 248 nat).(\forall (m: nat).((le n0 m) \to (P n0 m)))) in (let TMP_2 \def (\lambda
 249 (m: nat).(\lambda (_: (le O m)).(H m))) in (let TMP_14 \def (\lambda (n0:
 250 nat).(\lambda (IHn: ((\forall (m: nat).((le n0 m) \to (P n0 m))))).(\lambda
 251 (m: nat).(\lambda (Le: (le (S n0) m)).(let TMP_3 \def (S n0) in (let TMP_5
 252 \def (\lambda (n1: nat).(let TMP_4 \def (S n0) in (P TMP_4 n1))) in (let
 253 TMP_6 \def (le_n n0) in (let TMP_7 \def (le_n n0) in (let TMP_8 \def (IHn n0
 254 TMP_7) in (let TMP_9 \def (H0 n0 n0 TMP_6 TMP_8) in (let TMP_13 \def (\lambda
 255 (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_: (P (S n0) m0)).(let
 256 TMP_10 \def (le_trans_S n0 m0 H1) in (let TMP_11 \def (le_trans_S n0 m0 H1)
 257 in (let TMP_12 \def (IHn m0 TMP_11) in (H0 n0 m0 TMP_10 TMP_12))))))) in
 258 (le_ind TMP_3 TMP_5 TMP_9 TMP_13 m Le)))))))))))) in (nat_ind TMP_1 TMP_2
 259 TMP_14 n))))))).
 260
 261 theorem lt_n_n:
 262  \forall (n: nat).(not (lt n n))
 263 \def
 264  le_Sn_n.
 265
 266 theorem lt_n_S:
 267  \forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
 268 \def
 269  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(let TMP_1 \def (S
 270 n) in (le_n_S TMP_1 m H)))).
 271
 272 theorem lt_n_Sn:
 273  \forall (n: nat).(lt n (S n))
 274 \def
 275  \lambda (n: nat).(let TMP_1 \def (S n) in (le_n TMP_1)).
 276
 277 theorem lt_S_n:
 278  \forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
 279 \def
 280  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(let TMP_1
 281 \def (S n) in (le_S_n TMP_1 m H)))).
 282
 283 theorem lt_n_O:
 284  \forall (n: nat).(not (lt n O))
 285 \def
 286  le_Sn_O.
 287
 288 theorem lt_trans:
 289  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((lt m p)
 290 \to (lt n p)))))
 291 \def
 292  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 293 m)).(\lambda (H0: (lt m p)).(let TMP_1 \def (S m) in (let TMP_2 \def (\lambda
 294 (n0: nat).(lt n n0)) in (let TMP_3 \def (S n) in (let TMP_4 \def (le_S TMP_3
 295 m H) in (let TMP_6 \def (\lambda (m0: nat).(\lambda (_: (le (S m)
 296 m0)).(\lambda (IHle: (lt n m0)).(let TMP_5 \def (S n) in (le_S TMP_5 m0
 297 IHle))))) in (le_ind TMP_1 TMP_2 TMP_4 TMP_6 p H0)))))))))).
 298
 299 theorem lt_O_Sn:
 300  \forall (n: nat).(lt O (S n))
 301 \def
 302  \lambda (n: nat).(let TMP_1 \def (le_O_n n) in (le_n_S O n TMP_1)).
 303
 304 theorem lt_le_S:
 305  \forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
 306 \def
 307  \lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
 308
 309 theorem le_not_lt:
 310  \forall (n: nat).(\forall (m: nat).((le n m) \to (not (lt m n))))
 311 \def
 312  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(let TMP_2 \def
 313 (\lambda (n0: nat).(let TMP_1 \def (lt n0 n) in (not TMP_1))) in (let TMP_3
 314 \def (lt_n_n n) in (let TMP_6 \def (\lambda (m0: nat).(\lambda (_: (le n
 315 m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(let TMP_4
 316 \def (S m0) in (let TMP_5 \def (le_trans_S TMP_4 n H1) in (IHle TMP_5)))))))
 317 in (le_ind n TMP_2 TMP_3 TMP_6 m H)))))).
 318
 319 theorem le_lt_n_Sm:
 320  \forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
 321 \def
 322  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
 323
 324 theorem le_lt_trans:
 325  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((lt m p)
 326 \to (lt n p)))))
 327 \def
 328  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 329 m)).(\lambda (H0: (lt m p)).(let TMP_1 \def (S m) in (let TMP_2 \def (\lambda
 330 (n0: nat).(lt n n0)) in (let TMP_3 \def (le_n_S n m H) in (let TMP_5 \def
 331 (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt n
 332 m0)).(let TMP_4 \def (S n) in (le_S TMP_4 m0 IHle))))) in (le_ind TMP_1 TMP_2
 333 TMP_3 TMP_5 p H0))))))))).
 334
 335 theorem lt_le_trans:
 336  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((le m p)
 337 \to (lt n p)))))
 338 \def
 339  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 340 m)).(\lambda (H0: (le m p)).(let TMP_1 \def (\lambda (n0: nat).(lt n n0)) in
 341 (let TMP_3 \def (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle:
 342 (lt n m0)).(let TMP_2 \def (S n) in (le_S TMP_2 m0 IHle))))) in (le_ind m
 343 TMP_1 H TMP_3 p H0))))))).
 344
 345 theorem lt_le_weak:
 346  \forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
 347 \def
 348  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m
 349 H))).
 350
 351 theorem lt_n_Sm_le:
 352  \forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
 353 \def
 354  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m
 355 H))).
 356
 357 theorem le_lt_or_eq:
 358  \forall (n: nat).(\forall (m: nat).((le n m) \to (or (lt n m) (eq nat n m))))
 359 \def
 360  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(let TMP_3 \def
 361 (\lambda (n0: nat).(let TMP_1 \def (lt n n0) in (let TMP_2 \def (eq nat n n0)
 362 in (or TMP_1 TMP_2)))) in (let TMP_4 \def (lt n n) in (let TMP_5 \def (eq nat
 363 n n) in (let TMP_6 \def (refl_equal nat n) in (let TMP_7 \def (or_intror
 364 TMP_4 TMP_5 TMP_6) in (let TMP_13 \def (\lambda (m0: nat).(\lambda (H0: (le n
 365 m0)).(\lambda (_: (or (lt n m0) (eq nat n m0))).(let TMP_8 \def (S m0) in
 366 (let TMP_9 \def (lt n TMP_8) in (let TMP_10 \def (S m0) in (let TMP_11 \def
 367 (eq nat n TMP_10) in (let TMP_12 \def (le_n_S n m0 H0) in (or_introl TMP_9
 368 TMP_11 TMP_12))))))))) in (le_ind n TMP_3 TMP_7 TMP_13 m H))))))))).
 369
 370 theorem le_or_lt:
 371  \forall (n: nat).(\forall (m: nat).(or (le n m) (lt m n)))
 372 \def
 373  \lambda (n: nat).(\lambda (m: nat).(let TMP_3 \def (\lambda (n0:
 374 nat).(\lambda (n1: nat).(let TMP_1 \def (le n0 n1) in (let TMP_2 \def (lt n1
 375 n0) in (or TMP_1 TMP_2))))) in (let TMP_7 \def (\lambda (n0: nat).(let TMP_4
 376 \def (le O n0) in (let TMP_5 \def (lt n0 O) in (let TMP_6 \def (le_O_n n0) in
 377 (or_introl TMP_4 TMP_5 TMP_6))))) in (let TMP_15 \def (\lambda (n0: nat).(let
 378 TMP_8 \def (S n0) in (let TMP_9 \def (le TMP_8 O) in (let TMP_10 \def (S n0)
 379 in (let TMP_11 \def (lt O TMP_10) in (let TMP_12 \def (S n0) in (let TMP_13
 380 \def (lt_O_Sn n0) in (let TMP_14 \def (lt_le_S O TMP_12 TMP_13) in (or_intror
 381 TMP_9 TMP_11 TMP_14))))))))) in (let TMP_42 \def (\lambda (n0: nat).(\lambda
 382 (m0: nat).(\lambda (H: (or (le n0 m0) (lt m0 n0))).(let TMP_16 \def (le n0
 383 m0) in (let TMP_17 \def (lt m0 n0) in (let TMP_18 \def (S n0) in (let TMP_19
 384 \def (S m0) in (let TMP_20 \def (le TMP_18 TMP_19) in (let TMP_21 \def (S m0)
 385 in (let TMP_22 \def (S n0) in (let TMP_23 \def (lt TMP_21 TMP_22) in (let
 386 TMP_24 \def (or TMP_20 TMP_23) in (let TMP_32 \def (\lambda (H0: (le n0
 387 m0)).(let TMP_25 \def (S n0) in (let TMP_26 \def (S m0) in (let TMP_27 \def
 388 (le TMP_25 TMP_26) in (let TMP_28 \def (S m0) in (let TMP_29 \def (S n0) in
 389 (let TMP_30 \def (lt TMP_28 TMP_29) in (let TMP_31 \def (le_n_S n0 m0 H0) in
 390 (or_introl TMP_27 TMP_30 TMP_31))))))))) in (let TMP_41 \def (\lambda (H0:
 391 (lt m0 n0)).(let TMP_33 \def (S n0) in (let TMP_34 \def (S m0) in (let TMP_35
 392 \def (le TMP_33 TMP_34) in (let TMP_36 \def (S m0) in (let TMP_37 \def (S n0)
 393 in (let TMP_38 \def (lt TMP_36 TMP_37) in (let TMP_39 \def (S m0) in (let
 394 TMP_40 \def (le_n_S TMP_39 n0 H0) in (or_intror TMP_35 TMP_38
 395 TMP_40)))))))))) in (or_ind TMP_16 TMP_17 TMP_24 TMP_32 TMP_41
 396 H))))))))))))))) in (nat_double_ind TMP_3 TMP_7 TMP_15 TMP_42 n m)))))).
 397
 398 theorem plus_n_O:
 399  \forall (n: nat).(eq nat n (plus n O))
 400 \def
 401  \lambda (n: nat).(let TMP_2 \def (\lambda (n0: nat).(let TMP_1 \def (plus n0
 402 O) in (eq nat n0 TMP_1))) in (let TMP_3 \def (refl_equal nat O) in (let TMP_5
 403 \def (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0 O))).(let TMP_4 \def
 404 (plus n0 O) in (f_equal nat nat S n0 TMP_4 H)))) in (nat_ind TMP_2 TMP_3
 405 TMP_5 n)))).
 406
 407 theorem plus_n_Sm:
 408  \forall (n: nat).(\forall (m: nat).(eq nat (S (plus n m)) (plus n (S m))))
 409 \def
 410  \lambda (m: nat).(\lambda (n: nat).(let TMP_5 \def (\lambda (n0: nat).(let
 411 TMP_1 \def (plus n0 n) in (let TMP_2 \def (S TMP_1) in (let TMP_3 \def (S n)
 412 in (let TMP_4 \def (plus n0 TMP_3) in (eq nat TMP_2 TMP_4)))))) in (let TMP_6
 413 \def (S n) in (let TMP_7 \def (refl_equal nat TMP_6) in (let TMP_12 \def
 414 (\lambda (n0: nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S
 415 n)))).(let TMP_8 \def (plus n0 n) in (let TMP_9 \def (S TMP_8) in (let TMP_10
 416 \def (S n) in (let TMP_11 \def (plus n0 TMP_10) in (f_equal nat nat S TMP_9
 417 TMP_11 H))))))) in (nat_ind TMP_5 TMP_7 TMP_12 m)))))).
 418
 419 theorem plus_sym:
 420  \forall (n: nat).(\forall (m: nat).(eq nat (plus n m) (plus m n)))
 421 \def
 422  \lambda (n: nat).(\lambda (m: nat).(let TMP_3 \def (\lambda (n0: nat).(let
 423 TMP_1 \def (plus n0 m) in (let TMP_2 \def (plus m n0) in (eq nat TMP_1
 424 TMP_2)))) in (let TMP_4 \def (plus_n_O m) in (let TMP_16 \def (\lambda (y:
 425 nat).(\lambda (H: (eq nat (plus y m) (plus m y))).(let TMP_5 \def (plus m y)
 426 in (let TMP_6 \def (S TMP_5) in (let TMP_9 \def (\lambda (n0: nat).(let TMP_7
 427 \def (plus y m) in (let TMP_8 \def (S TMP_7) in (eq nat TMP_8 n0)))) in (let
 428 TMP_10 \def (plus y m) in (let TMP_11 \def (plus m y) in (let TMP_12 \def
 429 (f_equal nat nat S TMP_10 TMP_11 H) in (let TMP_13 \def (S y) in (let TMP_14
 430 \def (plus m TMP_13) in (let TMP_15 \def (plus_n_Sm m y) in (eq_ind nat TMP_6
 431 TMP_9 TMP_12 TMP_14 TMP_15)))))))))))) in (nat_ind TMP_3 TMP_4 TMP_16 n))))).
 432
 433 theorem plus_Snm_nSm:
 434  \forall (n: nat).(\forall (m: nat).(eq nat (plus (S n) m) (plus n (S m))))
 435 \def
 436  \lambda (n: nat).(\lambda (m: nat).(let TMP_1 \def (plus m n) in (let TMP_5
 437 \def (\lambda (n0: nat).(let TMP_2 \def (S n0) in (let TMP_3 \def (S m) in
 438 (let TMP_4 \def (plus n TMP_3) in (eq nat TMP_2 TMP_4))))) in (let TMP_6 \def
 439 (S m) in (let TMP_7 \def (plus TMP_6 n) in (let TMP_10 \def (\lambda (n0:
 440 nat).(let TMP_8 \def (plus m n) in (let TMP_9 \def (S TMP_8) in (eq nat TMP_9
 441 n0)))) in (let TMP_11 \def (S m) in (let TMP_12 \def (plus TMP_11 n) in (let
 442 TMP_13 \def (refl_equal nat TMP_12) in (let TMP_14 \def (S m) in (let TMP_15
 443 \def (plus n TMP_14) in (let TMP_16 \def (S m) in (let TMP_17 \def (plus_sym
 444 n TMP_16) in (let TMP_18 \def (eq_ind_r nat TMP_7 TMP_10 TMP_13 TMP_15
 445 TMP_17) in (let TMP_19 \def (plus n m) in (let TMP_20 \def (plus_sym n m) in
 446 (eq_ind_r nat TMP_1 TMP_5 TMP_18 TMP_19 TMP_20))))))))))))))))).
 447
 448 theorem plus_assoc_l:
 449  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus n (plus m
 450 p)) (plus (plus n m) p))))
 451 \def
 452  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(let TMP_5 \def
 453 (\lambda (n0: nat).(let TMP_1 \def (plus m p) in (let TMP_2 \def (plus n0
 454 TMP_1) in (let TMP_3 \def (plus n0 m) in (let TMP_4 \def (plus TMP_3 p) in
 455 (eq nat TMP_2 TMP_4)))))) in (let TMP_6 \def (plus m p) in (let TMP_7 \def
 456 (refl_equal nat TMP_6) in (let TMP_12 \def (\lambda (n0: nat).(\lambda (H:
 457 (eq nat (plus n0 (plus m p)) (plus (plus n0 m) p))).(let TMP_8 \def (plus m
 458 p) in (let TMP_9 \def (plus n0 TMP_8) in (let TMP_10 \def (plus n0 m) in (let
 459 TMP_11 \def (plus TMP_10 p) in (f_equal nat nat S TMP_9 TMP_11 H))))))) in
 460 (nat_ind TMP_5 TMP_7 TMP_12 n))))))).
 461
 462 theorem plus_assoc_r:
 463  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus (plus n
 464 m) p) (plus n (plus m p)))))
 465 \def
 466  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(let TMP_1 \def (plus m
 467 p) in (let TMP_2 \def (plus n TMP_1) in (let TMP_3 \def (plus n m) in (let
 468 TMP_4 \def (plus TMP_3 p) in (let TMP_5 \def (plus_assoc_l n m p) in (sym_eq
 469 nat TMP_2 TMP_4 TMP_5)))))))).
 470
 471 theorem simpl_plus_l:
 472  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus n m)
 473 (plus n p)) \to (eq nat m p))))
 474 \def
 475  \lambda (n: nat).(let TMP_1 \def (\lambda (n0: nat).(\forall (m:
 476 nat).(\forall (p: nat).((eq nat (plus n0 m) (plus n0 p)) \to (eq nat m p)))))
 477 in (let TMP_2 \def (\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat m
 478 p)).H))) in (let TMP_13 \def (\lambda (n0: nat).(\lambda (IHn: ((\forall (m:
 479 nat).(\forall (p: nat).((eq nat (plus n0 m) (plus n0 p)) \to (eq nat m
 480 p)))))).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat (S (plus n0
 481 m)) (S (plus n0 p)))).(let TMP_3 \def (plus n0 m) in (let TMP_4 \def (plus n0
 482 p) in (let TMP_5 \def (plus n0) in (let TMP_6 \def (plus n0 m) in (let TMP_7
 483 \def (plus n0 p) in (let TMP_8 \def (plus n0 m) in (let TMP_9 \def (plus n0
 484 p) in (let TMP_10 \def (eq_add_S TMP_8 TMP_9 H) in (let TMP_11 \def (f_equal
 485 nat nat TMP_5 TMP_6 TMP_7 TMP_10) in (let TMP_12 \def (IHn TMP_3 TMP_4
 486 TMP_11) in (IHn m p TMP_12)))))))))))))))) in (nat_ind TMP_1 TMP_2 TMP_13
 487 n)))).
 488
 489 theorem minus_n_O:
 490  \forall (n: nat).(eq nat n (minus n O))
 491 \def
 492  \lambda (n: nat).(let TMP_2 \def (\lambda (n0: nat).(let TMP_1 \def (minus
 493 n0 O) in (eq nat n0 TMP_1))) in (let TMP_3 \def (refl_equal nat O) in (let
 494 TMP_5 \def (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0 O))).(let
 495 TMP_4 \def (S n0) in (refl_equal nat TMP_4)))) in (nat_ind TMP_2 TMP_3 TMP_5
 496 n)))).
 497
 498 theorem minus_n_n:
 499  \forall (n: nat).(eq nat O (minus n n))
 500 \def
 501  \lambda (n: nat).(let TMP_2 \def (\lambda (n0: nat).(let TMP_1 \def (minus
 502 n0 n0) in (eq nat O TMP_1))) in (let TMP_3 \def (refl_equal nat O) in (let
 503 TMP_4 \def (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0 n0))).IHn))
 504 in (nat_ind TMP_2 TMP_3 TMP_4 n)))).
 505
 506 theorem minus_Sn_m:
 507  \forall (n: nat).(\forall (m: nat).((le m n) \to (eq nat (S (minus n m))
 508 (minus (S n) m))))
 509 \def
 510  \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le m n)).(let TMP_5 \def
 511 (\lambda (n0: nat).(\lambda (n1: nat).(let TMP_1 \def (minus n1 n0) in (let
 512 TMP_2 \def (S TMP_1) in (let TMP_3 \def (S n1) in (let TMP_4 \def (minus
 513 TMP_3 n0) in (eq nat TMP_2 TMP_4))))))) in (let TMP_10 \def (\lambda (p:
 514 nat).(let TMP_6 \def (minus p O) in (let TMP_7 \def (minus p O) in (let TMP_8
 515 \def (minus_n_O p) in (let TMP_9 \def (sym_eq nat p TMP_7 TMP_8) in (f_equal
 516 nat nat S TMP_6 p TMP_9)))))) in (let TMP_11 \def (\lambda (p: nat).(\lambda
 517 (q: nat).(\lambda (_: (le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match
 518 p with [O \Rightarrow (S q) | (S l) \Rightarrow (minus q l)]))).H0)))) in
 519 (le_elim_rel TMP_5 TMP_10 TMP_11 m n Le)))))).
 520
 521 theorem plus_minus:
 522  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat n (plus m p))
 523 \to (eq nat p (minus n m)))))
 524 \def
 525  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(let TMP_2 \def
 526 (\lambda (n0: nat).(\lambda (n1: nat).((eq nat n1 (plus n0 p)) \to (let TMP_1
 527 \def (minus n1 n0) in (eq nat p TMP_1))))) in (let TMP_7 \def (\lambda (n0:
 528 nat).(\lambda (H: (eq nat n0 p)).(let TMP_3 \def (\lambda (n1: nat).(eq nat p
 529 n1)) in (let TMP_4 \def (sym_eq nat n0 p H) in (let TMP_5 \def (minus n0 O)
 530 in (let TMP_6 \def (minus_n_O n0) in (eq_ind nat n0 TMP_3 TMP_4 TMP_5
 531 TMP_6))))))) in (let TMP_12 \def (\lambda (n0: nat).(\lambda (H: (eq nat O (S
 532 (plus n0 p)))).(let TMP_8 \def (eq nat p O) in (let H0 \def H in (let TMP_9
 533 \def (plus n0 p) in (let H1 \def (O_S TMP_9) in (let TMP_10 \def (\lambda
 534 (H2: (eq nat O (S (plus n0 p)))).(H1 H2)) in (let TMP_11 \def (TMP_10 H0) in
 535 (False_ind TMP_8 TMP_11))))))))) in (let TMP_15 \def (\lambda (n0:
 536 nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq nat p
 537 (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(let TMP_13
 538 \def (plus n0 p) in (let TMP_14 \def (eq_add_S m0 TMP_13 H0) in (H
 539 TMP_14))))))) in (nat_double_ind TMP_2 TMP_7 TMP_12 TMP_15 m n))))))).
 540
 541 theorem minus_plus:
 542  \forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
 543 \def
 544  \lambda (n: nat).(\lambda (m: nat).(let TMP_1 \def (plus n m) in (let TMP_2
 545 \def (minus TMP_1 n) in (let TMP_3 \def (plus n m) in (let TMP_4 \def (plus n
 546 m) in (let TMP_5 \def (refl_equal nat TMP_4) in (let TMP_6 \def (plus_minus
 547 TMP_3 n m TMP_5) in (sym_eq nat m TMP_2 TMP_6)))))))).
 548
 549 theorem le_pred_n:
 550  \forall (n: nat).(le (pred n) n)
 551 \def
 552  \lambda (n: nat).(let TMP_2 \def (\lambda (n0: nat).(let TMP_1 \def (pred
 553 n0) in (le TMP_1 n0))) in (let TMP_3 \def (le_n O) in (let TMP_7 \def
 554 (\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(let TMP_4 \def (S n0) in
 555 (let TMP_5 \def (pred TMP_4) in (let TMP_6 \def (le_n n0) in (le_S TMP_5 n0
 556 TMP_6)))))) in (nat_ind TMP_2 TMP_3 TMP_7 n)))).
 557
 558 theorem le_plus_l:
 559  \forall (n: nat).(\forall (m: nat).(le n (plus n m)))
 560 \def
 561  \lambda (n: nat).(let TMP_2 \def (\lambda (n0: nat).(\forall (m: nat).(let
 562 TMP_1 \def (plus n0 m) in (le n0 TMP_1)))) in (let TMP_3 \def (\lambda (m:
 563 nat).(le_O_n m)) in (let TMP_6 \def (\lambda (n0: nat).(\lambda (IHn:
 564 ((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(let TMP_4 \def
 565 (plus n0 m) in (let TMP_5 \def (IHn m) in (le_n_S n0 TMP_4 TMP_5)))))) in
 566 (nat_ind TMP_2 TMP_3 TMP_6 n)))).
 567
 568 theorem le_plus_r:
 569  \forall (n: nat).(\forall (m: nat).(le m (plus n m)))
 570 \def
 571  \lambda (n: nat).(\lambda (m: nat).(let TMP_2 \def (\lambda (n0: nat).(let
 572 TMP_1 \def (plus n0 m) in (le m TMP_1))) in (let TMP_3 \def (le_n m) in (let
 573 TMP_5 \def (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(let TMP_4
 574 \def (plus n0 m) in (le_S m TMP_4 H)))) in (nat_ind TMP_2 TMP_3 TMP_5 n))))).
 575
 576 theorem simpl_le_plus_l:
 577  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((le (plus p n) (plus p
 578 m)) \to (le n m))))
 579 \def
 580  \lambda (p: nat).(let TMP_1 \def (\lambda (n: nat).(\forall (n0:
 581 nat).(\forall (m: nat).((le (plus n n0) (plus n m)) \to (le n0 m))))) in (let
 582 TMP_2 \def (\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).H))) in
 583 (let TMP_6 \def (\lambda (p0: nat).(\lambda (IHp: ((\forall (n: nat).(\forall
 584 (m: nat).((le (plus p0 n) (plus p0 m)) \to (le n m)))))).(\lambda (n:
 585 nat).(\lambda (m: nat).(\lambda (H: (le (S (plus p0 n)) (S (plus p0
 586 m)))).(let TMP_3 \def (plus p0 n) in (let TMP_4 \def (plus p0 m) in (let
 587 TMP_5 \def (le_S_n TMP_3 TMP_4 H) in (IHp n m TMP_5))))))))) in (nat_ind
 588 TMP_1 TMP_2 TMP_6 p)))).
 589
 590 theorem le_plus_trans:
 591  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le n
 592 (plus m p)))))
 593 \def
 594  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 595 m)).(let TMP_1 \def (plus m p) in (let TMP_2 \def (le_plus_l m p) in
 596 (le_trans n m TMP_1 H TMP_2)))))).
 597
 598 theorem le_reg_l:
 599  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le (plus
 600 p n) (plus p m)))))
 601 \def
 602  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(let TMP_3 \def
 603 (\lambda (n0: nat).((le n m) \to (let TMP_1 \def (plus n0 n) in (let TMP_2
 604 \def (plus n0 m) in (le TMP_1 TMP_2))))) in (let TMP_4 \def (\lambda (H: (le
 605 n m)).H) in (let TMP_8 \def (\lambda (p0: nat).(\lambda (IHp: (((le n m) \to
 606 (le (plus p0 n) (plus p0 m))))).(\lambda (H: (le n m)).(let TMP_5 \def (plus
 607 p0 n) in (let TMP_6 \def (plus p0 m) in (let TMP_7 \def (IHp H) in (le_n_S
 608 TMP_5 TMP_6 TMP_7))))))) in (nat_ind TMP_3 TMP_4 TMP_8 p)))))).
 609
 610 theorem le_plus_plus:
 611  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
 612 n m) \to ((le p q) \to (le (plus n p) (plus m q)))))))
 613 \def
 614  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 615 nat).(\lambda (H: (le n m)).(\lambda (H0: (le p q)).(let TMP_3 \def (\lambda
 616 (n0: nat).(let TMP_1 \def (plus n p) in (let TMP_2 \def (plus n0 q) in (le
 617 TMP_1 TMP_2)))) in (let TMP_4 \def (le_reg_l p q n H0) in (let TMP_7 \def
 618 (\lambda (m0: nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus
 619 m0 q))).(let TMP_5 \def (plus n p) in (let TMP_6 \def (plus m0 q) in (le_S
 620 TMP_5 TMP_6 H2)))))) in (le_ind n TMP_3 TMP_4 TMP_7 m H))))))))).
 621
 622 theorem le_plus_minus:
 623  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus n (minus m
 624 n)))))
 625 \def
 626  \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le n m)).(let TMP_3 \def
 627 (\lambda (n0: nat).(\lambda (n1: nat).(let TMP_1 \def (minus n1 n0) in (let
 628 TMP_2 \def (plus n0 TMP_1) in (eq nat n1 TMP_2))))) in (let TMP_4 \def
 629 (\lambda (p: nat).(minus_n_O p)) in (let TMP_7 \def (\lambda (p:
 630 nat).(\lambda (q: nat).(\lambda (_: (le p q)).(\lambda (H0: (eq nat q (plus p
 631 (minus q p)))).(let TMP_5 \def (minus q p) in (let TMP_6 \def (plus p TMP_5)
 632 in (f_equal nat nat S q TMP_6 H0))))))) in (le_elim_rel TMP_3 TMP_4 TMP_7 n m
 633 Le)))))).
 634
 635 theorem le_plus_minus_r:
 636  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat (plus n (minus m
 637 n)) m)))
 638 \def
 639  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(let TMP_1 \def
 640 (minus m n) in (let TMP_2 \def (plus n TMP_1) in (let TMP_3 \def
 641 (le_plus_minus n m H) in (sym_eq nat m TMP_2 TMP_3)))))).
 642
 643 theorem simpl_lt_plus_l:
 644  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt (plus p n) (plus p
 645 m)) \to (lt n m))))
 646 \def
 647  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(let TMP_1 \def
 648 (\lambda (n0: nat).((lt (plus n0 n) (plus n0 m)) \to (lt n m))) in (let TMP_2
 649 \def (\lambda (H: (lt n m)).H) in (let TMP_7 \def (\lambda (p0: nat).(\lambda
 650 (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n m)))).(\lambda (H: (lt (S
 651 (plus p0 n)) (S (plus p0 m)))).(let TMP_3 \def (plus p0 n) in (let TMP_4 \def
 652 (S TMP_3) in (let TMP_5 \def (plus p0 m) in (let TMP_6 \def (le_S_n TMP_4
 653 TMP_5 H) in (IHp TMP_6)))))))) in (nat_ind TMP_1 TMP_2 TMP_7 p)))))).
 654
 655 theorem lt_reg_l:
 656  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
 657 p n) (plus p m)))))
 658 \def
 659  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(let TMP_3 \def
 660 (\lambda (n0: nat).((lt n m) \to (let TMP_1 \def (plus n0 n) in (let TMP_2
 661 \def (plus n0 m) in (lt TMP_1 TMP_2))))) in (let TMP_4 \def (\lambda (H: (lt
 662 n m)).H) in (let TMP_8 \def (\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to
 663 (lt (plus p0 n) (plus p0 m))))).(\lambda (H: (lt n m)).(let TMP_5 \def (plus
 664 p0 n) in (let TMP_6 \def (plus p0 m) in (let TMP_7 \def (IHp H) in (lt_n_S
 665 TMP_5 TMP_6 TMP_7))))))) in (nat_ind TMP_3 TMP_4 TMP_8 p)))))).
 666
 667 theorem lt_reg_r:
 668  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
 669 n p) (plus m p)))))
 670 \def
 671  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 672 m)).(let TMP_1 \def (plus p n) in (let TMP_3 \def (\lambda (n0: nat).(let
 673 TMP_2 \def (plus m p) in (lt n0 TMP_2))) in (let TMP_4 \def (plus p m) in
 674 (let TMP_6 \def (\lambda (n0: nat).(let TMP_5 \def (plus p n) in (lt TMP_5
 675 n0))) in (let TMP_9 \def (\lambda (n0: nat).(let TMP_7 \def (plus n0 n) in
 676 (let TMP_8 \def (plus n0 m) in (lt TMP_7 TMP_8)))) in (let TMP_11 \def
 677 (\lambda (n0: nat).(\lambda (_: (lt (plus n0 n) (plus n0 m))).(let TMP_10
 678 \def (S n0) in (lt_reg_l n m TMP_10 H)))) in (let TMP_12 \def (nat_ind TMP_9
 679 H TMP_11 p) in (let TMP_13 \def (plus m p) in (let TMP_14 \def (plus_sym m p)
 680 in (let TMP_15 \def (eq_ind_r nat TMP_4 TMP_6 TMP_12 TMP_13 TMP_14) in (let
 681 TMP_16 \def (plus n p) in (let TMP_17 \def (plus_sym n p) in (eq_ind_r nat
 682 TMP_1 TMP_3 TMP_15 TMP_16 TMP_17)))))))))))))))).
 683
 684 theorem le_lt_plus_plus:
 685  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
 686 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
 687 \def
 688  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 689 nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(let TMP_1 \def (S p)
 690 in (let TMP_2 \def (plus n TMP_1) in (let TMP_4 \def (\lambda (n0: nat).(let
 691 TMP_3 \def (plus m q) in (le n0 TMP_3))) in (let TMP_5 \def (S p) in (let
 692 TMP_6 \def (le_plus_plus n m TMP_5 q H H0) in (let TMP_7 \def (S n) in (let
 693 TMP_8 \def (plus TMP_7 p) in (let TMP_9 \def (plus_Snm_nSm n p) in (eq_ind_r
 694 nat TMP_2 TMP_4 TMP_6 TMP_8 TMP_9)))))))))))))).
 695
 696 theorem lt_le_plus_plus:
 697  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
 698 n m) \to ((le p q) \to (lt (plus n p) (plus m q)))))))
 699 \def
 700  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 701 nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(let TMP_1 \def (S n)
 702 in (le_plus_plus TMP_1 m p q H H0))))))).
 703
 704 theorem lt_plus_plus:
 705  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
 706 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
 707 \def
 708  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 709 nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(let TMP_1 \def
 710 (lt_le_weak p q H0) in (lt_le_plus_plus n m p q H TMP_1))))))).
 711
 712 theorem well_founded_ltof:
 713  \forall (A: Type[0]).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
 714 \def
 715  \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n:
 716 nat).(let TMP_2 \def (\lambda (n0: nat).(\forall (a: A).((lt (f a) n0) \to
 717 (let TMP_1 \def (ltof A f) in (Acc A TMP_1 a))))) in (let TMP_8 \def (\lambda
 718 (a: A).(\lambda (H: (lt (f a) O)).(let TMP_3 \def (ltof A f) in (let TMP_4
 719 \def (Acc A TMP_3 a) in (let H0 \def H in (let TMP_5 \def (f a) in (let H1
 720 \def (lt_n_O TMP_5) in (let TMP_6 \def (\lambda (H2: (lt (f a) O)).(H1 H2))
 721 in (let TMP_7 \def (TMP_6 H0) in (False_ind TMP_4 TMP_7)))))))))) in (let
 722 TMP_16 \def (\lambda (n0: nat).(\lambda (IHn: ((\forall (a: A).((lt (f a) n0)
 723 \to (Acc A (ltof A f) a))))).(\lambda (a: A).(\lambda (ltSma: (lt (f a) (S
 724 n0))).(let TMP_9 \def (ltof A f) in (let TMP_15 \def (\lambda (b: A).(\lambda
 725 (ltfafb: (lt (f b) (f a))).(let TMP_10 \def (f b) in (let TMP_11 \def (f a)
 726 in (let TMP_12 \def (f a) in (let TMP_13 \def (lt_n_Sm_le TMP_12 n0 ltSma) in
 727 (let TMP_14 \def (lt_le_trans TMP_10 TMP_11 n0 ltfafb TMP_13) in (IHn b
 728 TMP_14)))))))) in (Acc_intro A TMP_9 a TMP_15))))))) in (nat_ind TMP_2 TMP_8
 729 TMP_16 n))))) in (\lambda (a: A).(let TMP_17 \def (f a) in (let TMP_18 \def
 730 (S TMP_17) in (let TMP_19 \def (f a) in (let TMP_20 \def (S TMP_19) in (let
 731 TMP_21 \def (le_n TMP_20) in (H TMP_18 a TMP_21))))))))).
 732
 733 theorem lt_wf:
 734  well_founded nat lt
 735 \def
 736  let TMP_1 \def (\lambda (m: nat).m) in (well_founded_ltof nat TMP_1).
 737
 738 theorem lt_wf_ind:
 739  \forall (p: nat).(\forall (P: ((nat \to Prop))).(((\forall (n:
 740 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n)))) \to (P p)))
 741 \def
 742  \lambda (p: nat).(\lambda (P: ((nat \to Prop))).(\lambda (H: ((\forall (n:
 743 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n))))).(let TMP_1 \def
 744 (\lambda (n: nat).(P n)) in (let TMP_2 \def (\lambda (x: nat).(\lambda (_:
 745 ((\forall (y: nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall
 746 (y: nat).((lt y x) \to (P y))))).(H x H1)))) in (let TMP_3 \def (lt_wf p) in
 747 (Acc_ind nat lt TMP_1 TMP_2 p TMP_3)))))).
 748