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).(nat_ind (\lambda (n: nat).(\forall (n2: nat).(or (eq nat
  24 n n2) ((eq nat n n2) \to (\forall (P: Prop).P))))) (\lambda (n2:
  25 nat).(nat_ind (\lambda (n: nat).(or (eq nat O n) ((eq nat O n) \to (\forall
  26 (P: Prop).P)))) (or_introl (eq nat O O) ((eq nat O O) \to (\forall (P:
  27 Prop).P)) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (eq nat O n)
  28 ((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq
  29 nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S
  30 n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match
  31 ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _)
  32 \Rightarrow False])) I (S n) H0) in (False_ind P H1))))))) n2)) (\lambda (n:
  33 nat).(\lambda (H: ((\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to
  34 (\forall (P: Prop).P)))))).(\lambda (n2: nat).(nat_ind (\lambda (n0: nat).(or
  35 (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) (or_intror
  36 (eq nat (S n) O) ((eq nat (S n) O) \to (\forall (P: Prop).P)) (\lambda (H0:
  37 (eq nat (S n) O)).(\lambda (P: Prop).(let H1 \def (eq_ind nat (S n) (\lambda
  38 (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
  39 False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) (\lambda
  40 (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall
  41 (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P:
  42 Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P:
  43 Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0
  44 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P:
  45 Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S
  46 n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat
  47 (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat
  48 (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P:
  49 Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to
  50 (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P:
  51 Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return
  52 (\lambda (_: nat).nat) with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n)
  53 (S n0) H2) in (let H4 \def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3)
  54 \to (\forall (P0: Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0
  55 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0:
  56 Prop).P0)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2))))
  57 n1).
  58 (* COMMENTS
  59 Initial nodes: 676
  60 END *)
  61
  62 theorem simpl_plus_r:
  63  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n)
  64 (plus p n)) \to (eq nat m p))))
  65 \def
  66  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat
  67 (plus m n) (plus p n))).(simpl_plus_l n m p (eq_ind_r nat (plus m n) (\lambda
  68 (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0:
  69 nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_sym n
  70 p)) (plus m n) H) (plus n m) (plus_sym n m)))))).
  71 (* COMMENTS
  72 Initial nodes: 119
  73 END *)
  74
  75 theorem minus_Sx_Sy:
  76  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
  77 \def
  78  \lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
  79 (* COMMENTS
  80 Initial nodes: 13
  81 END *)
  82
  83 theorem minus_plus_r:
  84  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
  85 \def
  86  \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0:
  87 nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
  88 (* COMMENTS
  89 Initial nodes: 45
  90 END *)
  91
  92 theorem plus_permute_2_in_3:
  93  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x
  94 y) z) (plus (plus x z) y))))
  95 \def
  96  \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(eq_ind_r nat (plus x
  97 (plus y z)) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) (eq_ind_r nat
  98 (plus z y) (\lambda (n: nat).(eq nat (plus x n) (plus (plus x z) y))) (eq_ind
  99 nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y)))
 100 (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z
 101 y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
 102 (* COMMENTS
 103 Initial nodes: 163
 104 END *)
 105
 106 theorem plus_permute_2_in_3_assoc:
 107  \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n
 108 h) k) (plus n (plus k h)))))
 109 \def
 110  \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(eq_ind_r nat (plus
 111 (plus n k) h) (\lambda (n0: nat).(eq nat n0 (plus n (plus k h)))) (eq_ind_r
 112 nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0))
 113 (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k
 114 h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
 115 (* COMMENTS
 116 Initial nodes: 119
 117 END *)
 118
 119 theorem plus_O:
 120  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat
 121 x O) (eq nat y O))))
 122 \def
 123  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus
 124 n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda
 125 (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O)
 126 H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O)
 127 \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq
 128 nat (plus (S n) y) O)).(let H1 \def (match H0 in eq return (\lambda (n0:
 129 nat).(\lambda (_: (eq ? ? n0)).((eq nat n0 O) \to (land (eq nat (S n) O) (eq
 130 nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n)
 131 y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e in
 132 nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
 133 \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y
 134 O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
 135 (* COMMENTS
 136 Initial nodes: 233
 137 END *)
 138
 139 theorem minus_Sx_SO:
 140  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
 141 \def
 142  \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal
 143 nat x) (minus x O) (minus_n_O x)).
 144 (* COMMENTS
 145 Initial nodes: 33
 146 END *)
 147
 148 theorem eq_nat_dec:
 149  \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
 150 \def
 151  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq
 152 nat n j)) (eq nat n j)))) (\lambda (j: nat).(nat_ind (\lambda (n: nat).(or
 153 (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O)
 154 (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (not (eq nat O n)) (eq
 155 nat O n))).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j))
 156 (\lambda (n: nat).(\lambda (H: ((\forall (j: nat).(or (not (eq nat n j)) (eq
 157 nat n j))))).(\lambda (j: nat).(nat_ind (\lambda (n0: nat).(or (not (eq nat
 158 (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S
 159 n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda (n0: nat).(\lambda (_: (or
 160 (not (eq nat (S n) n0)) (eq nat (S n) n0))).(or_ind (not (eq nat n n0)) (eq
 161 nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda
 162 (H1: (not (eq nat n n0))).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S
 163 n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not
 164 (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H
 165 n0)))) j)))) i).
 166 (* COMMENTS
 167 Initial nodes: 401
 168 END *)
 169
 170 theorem neq_eq_e:
 171  \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j))
 172 \to P)) \to ((((eq nat i j) \to P)) \to P))))
 173 \def
 174  \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not
 175 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def
 176 (eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
 177 (* COMMENTS
 178 Initial nodes: 61
 179 END *)
 180
 181 theorem le_false:
 182  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S
 183 n) m) \to P))))
 184 \def
 185  \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P:
 186 Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P:
 187 Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match
 188 H0 in le return (\lambda (n0: nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to
 189 P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
 190 (eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_:
 191 nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in
 192 (False_ind P H2))) | (le_S m0 H1) \Rightarrow (\lambda (H2: (eq nat (S m0)
 193 O)).((let H3 \def (eq_ind nat (S m0) (\lambda (e: nat).(match e in nat return
 194 (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True]))
 195 I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1 (refl_equal
 196 nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P:
 197 Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind
 198 (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n))
 199 \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S
 200 O) (S n))).(let H2 \def (match H0 in le return (\lambda (n1: nat).(\lambda
 201 (_: (le ? n1)).((eq nat n1 O) \to P))) with [le_n \Rightarrow (\lambda (H2:
 202 (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e
 203 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
 204 \Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow
 205 (\lambda (H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda
 206 (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
 207 False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m0) \to P)
 208 H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_:
 209 ((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda
 210 (P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S
 211 n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
 212 (* COMMENTS
 213 Initial nodes: 409
 214 END *)
 215
 216 theorem le_Sx_x:
 217  \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
 218 \def
 219  \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def
 220 le_Sn_n in (False_ind P (H0 x H))))).
 221 (* COMMENTS
 222 Initial nodes: 23
 223 END *)
 224
 225 theorem le_n_pred:
 226  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
 227 \def
 228  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
 229 (n0: nat).(le (pred n) (pred n0))) (le_n (pred n)) (\lambda (m0:
 230 nat).(\lambda (_: (le n m0)).(\lambda (H1: (le (pred n) (pred m0))).(le_trans
 231 (pred n) (pred m0) m0 H1 (le_pred_n m0))))) m H))).
 232 (* COMMENTS
 233 Initial nodes: 71
 234 END *)
 235
 236 theorem minus_le:
 237  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
 238 \def
 239  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n
 240 y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall
 241 (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda (n0:
 242 nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: nat).(\lambda
 243 (_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)])
 244 (S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
 245 (* COMMENTS
 246 Initial nodes: 101
 247 END *)
 248
 249 theorem le_plus_minus_sym:
 250  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n)
 251 n))))
 252 \def
 253  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat
 254 (plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H)
 255 (plus (minus m n) n) (plus_sym (minus m n) n)))).
 256 (* COMMENTS
 257 Initial nodes: 61
 258 END *)
 259
 260 theorem le_minus_minus:
 261  \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z)
 262 \to (le (minus y x) (minus z x))))))
 263 \def
 264  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z:
 265 nat).(\lambda (H0: (le y z)).(simpl_le_plus_l x (minus y x) (minus z x)
 266 (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat
 267 z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z
 268 (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
 269 (* COMMENTS
 270 Initial nodes: 117
 271 END *)
 272
 273 theorem le_minus_plus:
 274  \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat
 275 (minus (plus x y) z) (plus (minus x z) y)))))
 276 \def
 277  \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to
 278 (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y))))))
 279 (\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le return
 280 (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) \to (\forall (y:
 281 nat).(eq nat (minus (plus x y) O) (plus (minus x O) y)))))) with [le_n
 282 \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n:
 283 nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))
 284 (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O)
 285 (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq
 286 nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y:
 287 nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O
 288 m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))])
 289 in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x:
 290 nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus
 291 (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S
 292 z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n
 293 (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def
 294 (match H0 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
 295 \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))))) with
 296 [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat
 297 (S z0) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with
 298 [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq
 299 nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1)
 300 \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m)
 301 (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
 302 \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S
 303 z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3))
 304 H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S
 305 z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n
 306 (S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n
 307 (le_S_n z0 n H1) y))))) x)))) z).
 308 (* COMMENTS
 309 Initial nodes: 603
 310 END *)
 311
 312 theorem le_minus:
 313  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to
 314 (le x (minus z y)))))
 315 \def
 316  \lambda (x: nat).(\lambda (z: nat).(\lambda (y: nat).(\lambda (H: (le (plus
 317 x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z
 318 y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x
 319 y))))).
 320 (* COMMENTS
 321 Initial nodes: 69
 322 END *)
 323
 324 theorem le_trans_plus_r:
 325  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to
 326 (le y z))))
 327 \def
 328  \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus
 329 x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
 330 (* COMMENTS
 331 Initial nodes: 35
 332 END *)
 333
 334 theorem lt_x_O:
 335  \forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
 336 \def
 337  \lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let H_y \def
 338 (le_n_O_eq (S x) H) in (let H0 \def (eq_ind nat O (\lambda (ee: nat).(match
 339 ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _)
 340 \Rightarrow False])) I (S x) H_y) in (False_ind P H0))))).
 341 (* COMMENTS
 342 Initial nodes: 48
 343 END *)
 344
 345 theorem le_gen_S:
 346  \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n:
 347 nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
 348 \def
 349  \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def
 350 (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x)
 351 \to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m
 352 n0)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat
 353 (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0)))
 354 (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S
 355 m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x
 356 H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat
 357 (S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq
 358 nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m)
 359 m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n:
 360 nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2))))
 361 x H1 H0))]) in (H0 (refl_equal nat x))))).
 362 (* COMMENTS
 363 Initial nodes: 261
 364 END *)
 365
 366 theorem lt_x_plus_x_Sy:
 367  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
 368 \def
 369  \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n:
 370 nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x))
 371 (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
 372 (* COMMENTS
 373 Initial nodes: 83
 374 END *)
 375
 376 theorem simpl_lt_plus_r:
 377  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m
 378 p)) \to (lt n m))))
 379 \def
 380  \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus
 381 n p) (plus m p))).(simpl_lt_plus_l n m p (let H0 \def (eq_ind nat (plus n p)
 382 (\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_sym n p)) in (let
 383 H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0
 384 (plus p m) (plus_sym m p)) in H1)))))).
 385 (* COMMENTS
 386 Initial nodes: 101
 387 END *)
 388
 389 theorem minus_x_Sy:
 390  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S
 391 (minus x (S y))))))
 392 \def
 393  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
 394 (eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H:
 395 (lt y O)).(let H0 \def (match H in le return (\lambda (n: nat).(\lambda (_:
 396 (le ? n)).((eq nat n O) \to (eq nat (minus O y) (S (minus O (S y))))))) with
 397 [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S
 398 y) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
 399 \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat
 400 (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda
 401 (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e:
 402 nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False
 403 | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat
 404 (minus O y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O)))))
 405 (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat
 406 (minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0:
 407 nat).((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))))
 408 (\lambda (_: (lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S
 409 n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0:
 410 nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S
 411 n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0)
 412 n H1) in (H n0 H2))))) y)))) x).
 413 (* COMMENTS
 414 Initial nodes: 383
 415 END *)
 416
 417 theorem lt_plus_minus:
 418  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus
 419 y (S x)))))))
 420 \def
 421  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S
 422 x) y H))).
 423 (* COMMENTS
 424 Initial nodes: 19
 425 END *)
 426
 427 theorem lt_plus_minus_r:
 428  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y
 429 (S x)) x)))))
 430 \def
 431  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat
 432 (plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x
 433 y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
 434 (* COMMENTS
 435 Initial nodes: 69
 436 END *)
 437
 438 theorem minus_x_SO:
 439  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
 440 \def
 441  \lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n:
 442 nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal
 443 nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
 444 (* COMMENTS
 445 Initial nodes: 77
 446 END *)
 447
 448 theorem le_x_pred_y:
 449  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
 450 \def
 451  \lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to
 452 (le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def
 453 (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
 454 \to (le x O)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let
 455 H1 \def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat return (\lambda
 456 (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0)
 457 in (False_ind (le x O) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat
 458 (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat
 459 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
 460 True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0
 461 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt
 462 x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S
 463 n))).(le_S_n x n H0))))) y).
 464 (* COMMENTS
 465 Initial nodes: 189
 466 END *)
 467
 468 theorem lt_le_minus:
 469  \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
 470 \def
 471  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S
 472 O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O))
 473 (plus_sym x (S O)))))).
 474 (* COMMENTS
 475 Initial nodes: 57
 476 END *)
 477
 478 theorem lt_le_e:
 479  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P))
 480 \to ((((le d n) \to P)) \to P))))
 481 \def
 482  \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n
 483 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in
 484 (or_ind (le d n) (lt n d) P H0 H H1)))))).
 485 (* COMMENTS
 486 Initial nodes: 49
 487 END *)
 488
 489 theorem lt_eq_e:
 490  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
 491 \to ((((eq nat x y) \to P)) \to ((le x y) \to P)))))
 492 \def
 493  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x
 494 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x
 495 y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
 496 (* COMMENTS
 497 Initial nodes: 59
 498 END *)
 499
 500 theorem lt_eq_gt_e:
 501  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P))
 502 \to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P)))))
 503 \def
 504  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x
 505 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x)
 506 \to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda
 507 (H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
 508 (* COMMENTS
 509 Initial nodes: 79
 510 END *)
 511
 512 theorem lt_gen_xS:
 513  \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2
 514 nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n))))))
 515 \def
 516  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).((lt n (S
 517 n0)) \to (or (eq nat n O) (ex2 nat (\lambda (m: nat).(eq nat n (S m)))
 518 (\lambda (m: nat).(lt m n0))))))) (\lambda (n: nat).(\lambda (_: (lt O (S
 519 n))).(or_introl (eq nat O O) (ex2 nat (\lambda (m: nat).(eq nat O (S m)))
 520 (\lambda (m: nat).(lt m n))) (refl_equal nat O)))) (\lambda (n: nat).(\lambda
 521 (_: ((\forall (n0: nat).((lt n (S n0)) \to (or (eq nat n O) (ex2 nat (\lambda
 522 (m: nat).(eq nat n (S m))) (\lambda (m: nat).(lt m n0)))))))).(\lambda (n0:
 523 nat).(\lambda (H0: (lt (S n) (S n0))).(or_intror (eq nat (S n) O) (ex2 nat
 524 (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0)))
 525 (ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt
 526 m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
 527 (* COMMENTS
 528 Initial nodes: 243
 529 END *)
 530
 531 theorem le_lt_false:
 532  \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P:
 533 Prop).P))))
 534 \def
 535  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt
 536 y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
 537 (* COMMENTS
 538 Initial nodes: 31
 539 END *)
 540
 541 theorem lt_neq:
 542  \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
 543 \def
 544  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq
 545 nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in
 546 (lt_n_n y H1))))).
 547 (* COMMENTS
 548 Initial nodes: 43
 549 END *)
 550
 551 theorem arith0:
 552  \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n)
 553 \to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2))))))
 554 \def
 555  \lambda (h2: nat).(\lambda (d2: nat).(\lambda (n: nat).(\lambda (H: (le
 556 (plus d2 h2) n)).(\lambda (h1: nat).(eq_ind nat (minus (plus h2 (plus d2 h1))
 557 h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2
 558 (plus h2 (plus d2 h1)) (le_plus_l h2 (plus d2 h1)) (plus n h1) (eq_ind_r nat
 559 (plus (plus h2 d2) h1) (\lambda (n0: nat).(le n0 (plus n h1))) (eq_ind_r nat
 560 (plus d2 h2) (\lambda (n0: nat).(le (plus n0 h1) (plus n h1))) (le_S_n (plus
 561 (plus d2 h2) h1) (plus n h1) (le_n_S (plus (plus d2 h2) h1) (plus n h1)
 562 (le_plus_plus (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_sym h2
 563 d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1)
 564 (minus_plus h2 (plus d2 h1))))))).
 565 (* COMMENTS
 566 Initial nodes: 235
 567 END *)
 568
 569 theorem O_minus:
 570  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
 571 \def
 572  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to
 573 (eq nat (minus n y) O)))) (\lambda (y: nat).(\lambda (_: (le O
 574 y)).(refl_equal nat O))) (\lambda (x0: nat).(\lambda (H: ((\forall (y:
 575 nat).((le x0 y) \to (eq nat (minus x0 y) O))))).(\lambda (y: nat).(nat_ind
 576 (\lambda (n: nat).((le (S x0) n) \to (eq nat (match n with [O \Rightarrow (S
 577 x0) | (S l) \Rightarrow (minus x0 l)]) O))) (\lambda (H0: (le (S x0)
 578 O)).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le x0
 579 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H1: (eq nat O (S
 580 x1))).(\lambda (_: (le x0 x1)).(let H3 \def (eq_ind nat O (\lambda (ee:
 581 nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
 582 | (S _) \Rightarrow False])) I (S x1) H1) in (False_ind (eq nat (S x0) O)
 583 H3))))) (le_gen_S x0 O H0))) (\lambda (n: nat).(\lambda (_: (((le (S x0) n)
 584 \to (eq nat (match n with [O \Rightarrow (S x0) | (S l) \Rightarrow (minus x0
 585 l)]) O)))).(\lambda (H1: (le (S x0) (S n))).(H n (le_S_n x0 n H1))))) y))))
 586 x).
 587 (* COMMENTS
 588 Initial nodes: 252
 589 END *)
 590
 591 theorem minus_minus:
 592  \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y)
 593 \to ((eq nat (minus x z) (minus y z)) \to (eq nat x y))))))
 594 \def
 595  \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).(\forall (y:
 596 nat).((le n x) \to ((le n y) \to ((eq nat (minus x n) (minus y n)) \to (eq
 597 nat x y))))))) (\lambda (x: nat).(\lambda (y: nat).(\lambda (_: (le O
 598 x)).(\lambda (_: (le O y)).(\lambda (H1: (eq nat (minus x O) (minus y
 599 O))).(let H2 \def (eq_ind_r nat (minus x O) (\lambda (n: nat).(eq nat n
 600 (minus y O))) H1 x (minus_n_O x)) in (let H3 \def (eq_ind_r nat (minus y O)
 601 (\lambda (n: nat).(eq nat x n)) H2 y (minus_n_O y)) in H3))))))) (\lambda
 602 (z0: nat).(\lambda (IH: ((\forall (x: nat).(\forall (y: nat).((le z0 x) \to
 603 ((le z0 y) \to ((eq nat (minus x z0) (minus y z0)) \to (eq nat x
 604 y)))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le
 605 (S z0) n) \to ((le (S z0) y) \to ((eq nat (minus n (S z0)) (minus y (S z0)))
 606 \to (eq nat n y)))))) (\lambda (y: nat).(\lambda (H: (le (S z0) O)).(\lambda
 607 (_: (le (S z0) y)).(\lambda (_: (eq nat (minus O (S z0)) (minus y (S
 608 z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le
 609 z0 n)) (eq nat O y) (\lambda (x0: nat).(\lambda (H2: (eq nat O (S
 610 x0))).(\lambda (_: (le z0 x0)).(let H4 \def (eq_ind nat O (\lambda (ee:
 611 nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
 612 | (S _) \Rightarrow False])) I (S x0) H2) in (False_ind (eq nat O y) H4)))))
 613 (le_gen_S z0 O H)))))) (\lambda (x0: nat).(\lambda (_: ((\forall (y:
 614 nat).((le (S z0) x0) \to ((le (S z0) y) \to ((eq nat (minus x0 (S z0)) (minus
 615 y (S z0))) \to (eq nat x0 y))))))).(\lambda (y: nat).(nat_ind (\lambda (n:
 616 nat).((le (S z0) (S x0)) \to ((le (S z0) n) \to ((eq nat (minus (S x0) (S
 617 z0)) (minus n (S z0))) \to (eq nat (S x0) n))))) (\lambda (H: (le (S z0) (S
 618 x0))).(\lambda (H0: (le (S z0) O)).(\lambda (_: (eq nat (minus (S x0) (S z0))
 619 (minus O (S z0)))).(let H_y \def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda
 620 (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le z0 n)) (eq nat (S x0) O)
 621 (\lambda (x1: nat).(\lambda (H2: (eq nat O (S x1))).(\lambda (_: (le z0
 622 x1)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat return
 623 (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
 624 I (S x1) H2) in (False_ind (eq nat (S x0) O) H4))))) (le_gen_S z0 O H0))))))
 625 (\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to
 626 ((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0)
 627 y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S
 628 y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S
 629 z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0)
 630 H1))))))) y)))) x)))) z).
 631 (* COMMENTS
 632 Initial nodes: 751
 633 END *)
 634
 635 theorem plus_plus:
 636  \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1:
 637 nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z
 638 x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1)))))))))
 639 \def
 640  \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x1: nat).(\forall (x2:
 641 nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 n) \to ((le x2 n) \to ((eq
 642 nat (plus (minus n x1) y1) (plus (minus n x2) y2)) \to (eq nat (plus x1 y2)
 643 (plus x2 y1)))))))))) (\lambda (x1: nat).(\lambda (x2: nat).(\lambda (y1:
 644 nat).(\lambda (y2: nat).(\lambda (H: (le x1 O)).(\lambda (H0: (le x2
 645 O)).(\lambda (H1: (eq nat y1 y2)).(eq_ind nat y1 (\lambda (n: nat).(eq nat
 646 (plus x1 n) (plus x2 y1))) (let H_y \def (le_n_O_eq x2 H0) in (eq_ind nat O
 647 (\lambda (n: nat).(eq nat (plus x1 y1) (plus n y1))) (let H_y0 \def
 648 (le_n_O_eq x1 H) in (eq_ind nat O (\lambda (n: nat).(eq nat (plus n y1) (plus
 649 O y1))) (refl_equal nat (plus O y1)) x1 H_y0)) x2 H_y)) y2 H1))))))))
 650 (\lambda (z0: nat).(\lambda (IH: ((\forall (x1: nat).(\forall (x2:
 651 nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z0) \to ((le x2 z0) \to
 652 ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2)) \to (eq nat (plus
 653 x1 y2) (plus x2 y1))))))))))).(\lambda (x1: nat).(nat_ind (\lambda (n:
 654 nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le n (S z0))
 655 \to ((le x2 (S z0)) \to ((eq nat (plus (minus (S z0) n) y1) (plus (minus (S
 656 z0) x2) y2)) \to (eq nat (plus n y2) (plus x2 y1))))))))) (\lambda (x2:
 657 nat).(nat_ind (\lambda (n: nat).(\forall (y1: nat).(\forall (y2: nat).((le O
 658 (S z0)) \to ((le n (S z0)) \to ((eq nat (plus (minus (S z0) O) y1) (plus
 659 (minus (S z0) n) y2)) \to (eq nat (plus O y2) (plus n y1)))))))) (\lambda
 660 (y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda (_: (le O
 661 (S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (S (plus z0 y2)))).(let H_y
 662 \def (IH O O) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n:
 663 nat).(\forall (y3: nat).(\forall (y4: nat).((le O z0) \to ((le O z0) \to ((eq
 664 nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) H_y z0 (minus_n_O z0))
 665 in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (eq_add_S (plus z0 y1) (plus z0 y2)
 666 H1))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2:
 667 nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) (plus
 668 (match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2))
 669 \to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2:
 670 nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S x3) (S z0))).(\lambda
 671 (H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2))).(let H_y \def (IH O
 672 x3 (S y1)) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n:
 673 nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S
 674 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H_y z0
 675 (minus_n_O z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda (n:
 676 nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus
 677 (minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1))
 678 (plus_n_Sm z0 y1)) in (let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda
 679 (n: nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus
 680 z0 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 n)))))) H3 (S (plus x3 y1))
 681 (plus_n_Sm x3 y1)) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1))))))))))))
 682 x2)) (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall (y1:
 683 nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat
 684 (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2
 685 y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(nat_ind (\lambda (n:
 686 nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S
 687 z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2))
 688 \to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda (y1: nat).(\lambda
 689 (y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (_: (le O (S
 690 z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))).(let
 691 H_y \def (IH x2 O y1 (S y2)) in (let H2 \def (eq_ind_r nat (minus z0 O)
 692 (\lambda (n: nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2)
 693 y1) (plus n (S y2))) \to (eq nat (plus x2 (S y2)) y1))))) H_y z0 (minus_n_O
 694 z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda (n: nat).((le x2
 695 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (eq nat (plus
 696 x2 (S y2)) y1))))) H2 (S (plus z0 y2)) (plus_n_Sm z0 y2)) in (let H4 \def
 697 (eq_ind_r nat (plus x2 (S y2)) (\lambda (n: nat).((le x2 z0) \to ((le O z0)
 698 \to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1)))))
 699 H3 (S (plus x2 y2)) (plus_n_Sm x2 y2)) in (H4 (le_S_n x2 z0 H) (le_O_n z0)
 700 H1)))))))))) (\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall
 701 (y2: nat).((le (S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus
 702 z0 x2) y1) (plus (match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow
 703 (minus z0 l)]) y2)) \to (eq nat (S (plus x2 y2)) (plus x4
 704 y1))))))))).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S
 705 z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0
 706 x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4
 707 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3))))
 708 x1)))) z).
 709 (* COMMENTS
 710 Initial nodes: 1495
 711 END *)
 712
 713 theorem le_S_minus:
 714  \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to
 715 (le d (S (minus n h))))))
 716 \def
 717  \lambda (d: nat).(\lambda (h: nat).(\lambda (n: nat).(\lambda (H: (le (plus
 718 d h) n)).(let H0 \def (le_trans d (plus d h) n (le_plus_l d h) H) in (let H1
 719 \def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus n h) h)
 720 (le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S
 721 d (minus n h) (le_minus d n h H))))))).
 722 (* COMMENTS
 723 Initial nodes: 107
 724 END *)
 725
 726 theorem lt_x_pred_y:
 727  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
 728 \def
 729  \lambda (x: nat).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((lt x (pred
 730 n)) \to (lt (S x) n))) (\lambda (H: (lt x O)).(lt_x_O x H (lt (S x) O)))
 731 (\lambda (n: nat).(\lambda (_: (((lt x (pred n)) \to (lt (S x) n)))).(\lambda
 732 (H0: (lt x n)).(le_S_n (S (S x)) (S n) (le_n_S (S (S x)) (S n) (le_n_S (S x)
 733 n H0)))))) y)).
 734 (* COMMENTS
 735 Initial nodes: 103
 736 END *)
 737