matita/matita/contribs/lambdadelta/legacy_1A/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_1A/coq/fwd.ma".
  18
  19 lemma 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)).(eq_ind A x
  25 (\lambda (a: A).(eq B (f x) (f a))) (refl_equal B (f x)) y H)))))).
  26
  27 lemma f_equal2:
  28  \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (B: Type[0]).(\forall
  29 (f: ((A1 \to (A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2:
  30 A2).(\forall (y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2)
  31 (f y1 y2)))))))))))
  32 \def
  33  \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (B: Type[0]).(\lambda
  34 (f: ((A1 \to (A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2:
  35 A2).(\lambda (y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a:
  36 A1).((eq A2 x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2
  37 y2)).(eq_ind A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B
  38 (f x1 x2)) y2 H0)) y1 H))))))))).
  39
  40 lemma f_equal3:
  41  \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (A3: Type[0]).(\forall
  42 (B: Type[0]).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1:
  43 A1).(\forall (y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3:
  44 A3).(\forall (y3: A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3)
  45 \to (eq B (f x1 x2 x3) (f y1 y2 y3)))))))))))))))
  46 \def
  47  \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (A3: Type[0]).(\lambda
  48 (B: Type[0]).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1:
  49 A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3:
  50 A3).(\lambda (y3: A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a:
  51 A1).((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3)))))
  52 (\lambda (H0: (eq A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3)
  53 \to (eq B (f x1 x2 x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3
  54 x3 (\lambda (a: A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2
  55 x3)) y3 H1)) y2 H0)) y1 H)))))))))))).
  56
  57 lemma sym_eq:
  58  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y
  59 x))))
  60 \def
  61  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x
  62 y)).(eq_ind A x (\lambda (a: A).(eq A a x)) (refl_equal A x) y H)))).
  63
  64 lemma eq_ind_r:
  65  \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to
  66 (\forall (y: A).((eq A y x) \to (P y))))))
  67 \def
  68  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda
  69 (H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0)
  70 with [refl_equal \Rightarrow H])))))).
  71
  72 lemma trans_eq:
  73  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A
  74 x y) \to ((eq A y z) \to (eq A x z))))))
  75 \def
  76  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (z:
  77 A).(\lambda (H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda
  78 (a: A).(eq A x a)) H z H0)))))).
  79
  80 lemma sym_not_eq:
  81  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to
  82 (not (eq A y x)))))
  83 \def
  84  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq
  85 A x y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a
  86 y)) (refl_equal A y) x h2)))))).
  87
  88 lemma nat_double_ind:
  89  \forall (R: ((nat \to (nat \to Prop)))).(((\forall (n: nat).(R O n))) \to
  90 (((\forall (n: nat).(R (S n) O))) \to (((\forall (n: nat).(\forall (m:
  91 nat).((R n m) \to (R (S n) (S m)))))) \to (\forall (n: nat).(\forall (m:
  92 nat).(R n m))))))
  93 \def
  94  \lambda (R: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (n: nat).(R O
  95 n)))).(\lambda (H0: ((\forall (n: nat).(R (S n) O)))).(\lambda (H1: ((\forall
  96 (n: nat).(\forall (m: nat).((R n m) \to (R (S n) (S m))))))).(\lambda (n:
  97 nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(R n0 m))) H (\lambda (n0:
  98 nat).(\lambda (H2: ((\forall (m: nat).(R n0 m)))).(\lambda (m: nat).(nat_ind
  99 (\lambda (n1: nat).(R (S n0) n1)) (H0 n0) (\lambda (n1: nat).(\lambda (_: (R
 100 (S n0) n1)).(H1 n0 n1 (H2 n1)))) m)))) n))))).
 101
 102 lemma eq_add_S:
 103  \forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
 104 \def
 105  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S
 106 m))).(f_equal nat nat pred (S n) (S m) H))).
 107
 108 lemma O_S:
 109  \forall (n: nat).(not (eq nat O (S n)))
 110 \def
 111  \lambda (n: nat).(\lambda (H: (eq nat O (S n))).(eq_ind nat (S n) (\lambda
 112 (n0: nat).(IsSucc n0)) I O (sym_eq nat O (S n) H))).
 113
 114 lemma not_eq_S:
 115  \forall (n: nat).(\forall (m: nat).((not (eq nat n m)) \to (not (eq nat (S
 116 n) (S m)))))
 117 \def
 118  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda
 119 (H0: (eq nat (S n) (S m))).(H (eq_add_S n m H0))))).
 120
 121 lemma pred_Sn:
 122  \forall (m: nat).(eq nat m (pred (S m)))
 123 \def
 124  \lambda (m: nat).(refl_equal nat (pred (S m))).
 125
 126 lemma S_pred:
 127  \forall (n: nat).(\forall (m: nat).((lt m n) \to (eq nat n (S (pred n)))))
 128 \def
 129  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt m n)).(le_ind (S m)
 130 (\lambda (n0: nat).(eq nat n0 (S (pred n0)))) (refl_equal nat (S (pred (S
 131 m)))) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (_: (eq nat m0
 132 (S (pred m0)))).(refl_equal nat (S (pred (S m0))))))) n H))).
 133
 134 lemma le_trans:
 135  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((le m p)
 136 \to (le n p)))))
 137 \def
 138  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 139 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(le n n0)) H
 140 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (le n m0)).(le_S n
 141 m0 IHle)))) p H0))))).
 142
 143 lemma le_trans_S:
 144  \forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
 145 \def
 146  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(le_trans n (S
 147 n) m (le_S n n (le_n n)) H))).
 148
 149 lemma le_n_S:
 150  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
 151 \def
 152  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
 153 (n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
 154 n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
 155
 156 lemma le_O_n:
 157  \forall (n: nat).(le O n)
 158 \def
 159  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le O n0)) (le_n O) (\lambda
 160 (n0: nat).(\lambda (IHn: (le O n0)).(le_S O n0 IHn))) n).
 161
 162 lemma le_S_n:
 163  \forall (n: nat).(\forall (m: nat).((le (S n) (S m)) \to (le n m)))
 164 \def
 165  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) (S m))).(le_ind (S
 166 n) (\lambda (n0: nat).(le (pred (S n)) (pred n0))) (le_n n) (\lambda (m0:
 167 nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S
 168 n m0 H0)))) (S m) H))).
 169
 170 lemma le_Sn_O:
 171  \forall (n: nat).(not (le (S n) O))
 172 \def
 173  \lambda (n: nat).(\lambda (H: (le (S n) O)).(le_ind (S n) (\lambda (n0:
 174 nat).(IsSucc n0)) I (\lambda (m: nat).(\lambda (_: (le (S n) m)).(\lambda (_:
 175 (IsSucc m)).I))) O H)).
 176
 177 lemma le_Sn_n:
 178  \forall (n: nat).(not (le (S n) n))
 179 \def
 180  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(not (le (S n0) n0))) (le_Sn_O
 181 O) (\lambda (n0: nat).(\lambda (IHn: (not (le (S n0) n0))).(\lambda (H: (le
 182 (S (S n0)) (S n0))).(IHn (le_S_n (S n0) n0 H))))) n).
 183
 184 lemma le_antisym:
 185  \forall (n: nat).(\forall (m: nat).((le n m) \to ((le m n) \to (eq nat n
 186 m))))
 187 \def
 188  \lambda (n: nat).(\lambda (m: nat).(\lambda (h: (le n m)).(le_ind n (\lambda
 189 (n0: nat).((le n0 n) \to (eq nat n n0))) (\lambda (_: (le n n)).(refl_equal
 190 nat n)) (\lambda (m0: nat).(\lambda (H: (le n m0)).(\lambda (_: (((le m0 n)
 191 \to (eq nat n m0)))).(\lambda (H1: (le (S m0) n)).(False_ind (eq nat n (S
 192 m0)) (let H2 \def (le_trans (S m0) n m0 H1 H) in ((let H3 \def (le_Sn_n m0)
 193 in (\lambda (H4: (le (S m0) m0)).(H3 H4))) H2))))))) m h))).
 194
 195 lemma le_n_O_eq:
 196  \forall (n: nat).((le n O) \to (eq nat O n))
 197 \def
 198  \lambda (n: nat).(\lambda (H: (le n O)).(le_antisym O n (le_O_n n) H)).
 199
 200 lemma le_elim_rel:
 201  \forall (P: ((nat \to (nat \to Prop)))).(((\forall (p: nat).(P O p))) \to
 202 (((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p q) \to (P (S p) (S
 203 q))))))) \to (\forall (n: nat).(\forall (m: nat).((le n m) \to (P n m))))))
 204 \def
 205  \lambda (P: ((nat \to (nat \to Prop)))).(\lambda (H: ((\forall (p: nat).(P O
 206 p)))).(\lambda (H0: ((\forall (p: nat).(\forall (q: nat).((le p q) \to ((P p
 207 q) \to (P (S p) (S q)))))))).(\lambda (n: nat).(nat_ind (\lambda (n0:
 208 nat).(\forall (m: nat).((le n0 m) \to (P n0 m)))) (\lambda (m: nat).(\lambda
 209 (_: (le O m)).(H m))) (\lambda (n0: nat).(\lambda (IHn: ((\forall (m:
 210 nat).((le n0 m) \to (P n0 m))))).(\lambda (m: nat).(\lambda (Le: (le (S n0)
 211 m)).(le_ind (S n0) (\lambda (n1: nat).(P (S n0) n1)) (H0 n0 n0 (le_n n0) (IHn
 212 n0 (le_n n0))) (\lambda (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_:
 213 (P (S n0) m0)).(H0 n0 m0 (le_trans_S n0 m0 H1) (IHn m0 (le_trans_S n0 m0
 214 H1)))))) m Le))))) n)))).
 215
 216 lemma lt_n_n:
 217  \forall (n: nat).(not (lt n n))
 218 \def
 219  le_Sn_n.
 220
 221 lemma lt_n_S:
 222  \forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
 223 \def
 224  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_n_S (S n) m
 225 H))).
 226
 227 lemma lt_n_Sn:
 228  \forall (n: nat).(lt n (S n))
 229 \def
 230  \lambda (n: nat).(le_n (S n)).
 231
 232 lemma lt_S_n:
 233  \forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
 234 \def
 235  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(le_S_n (S
 236 n) m H))).
 237
 238 lemma lt_n_O:
 239  \forall (n: nat).(not (lt n O))
 240 \def
 241  le_Sn_O.
 242
 243 lemma lt_trans:
 244  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((lt m p)
 245 \to (lt n p)))))
 246 \def
 247  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 248 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) (le_S
 249 (S n) m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt
 250 n m0)).(le_S (S n) m0 IHle)))) p H0))))).
 251
 252 lemma lt_O_Sn:
 253  \forall (n: nat).(lt O (S n))
 254 \def
 255  \lambda (n: nat).(le_n_S O n (le_O_n n)).
 256
 257 lemma lt_le_S:
 258  \forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
 259 \def
 260  \lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
 261
 262 lemma le_not_lt:
 263  \forall (n: nat).(\forall (m: nat).((le n m) \to (not (lt m n))))
 264 \def
 265  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
 266 (n0: nat).(not (lt n0 n))) (lt_n_n n) (\lambda (m0: nat).(\lambda (_: (le n
 267 m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(IHle
 268 (le_trans_S (S m0) n H1)))))) m H))).
 269
 270 lemma le_lt_n_Sm:
 271  \forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
 272 \def
 273  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
 274
 275 lemma le_lt_trans:
 276  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((lt m p)
 277 \to (lt n p)))))
 278 \def
 279  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 280 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0))
 281 (le_n_S n m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle:
 282 (lt n m0)).(le_S (S n) m0 IHle)))) p H0))))).
 283
 284 lemma lt_le_trans:
 285  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((le m p)
 286 \to (lt n p)))))
 287 \def
 288  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 289 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(lt n n0)) H
 290 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (lt n m0)).(le_S
 291 (S n) m0 IHle)))) p H0))))).
 292
 293 lemma lt_le_weak:
 294  \forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
 295 \def
 296  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m
 297 H))).
 298
 299 lemma lt_n_Sm_le:
 300  \forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
 301 \def
 302  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m
 303 H))).
 304
 305 lemma le_lt_or_eq:
 306  \forall (n: nat).(\forall (m: nat).((le n m) \to (or (lt n m) (eq nat n m))))
 307 \def
 308  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
 309 (n0: nat).(or (lt n n0) (eq nat n n0))) (or_intror (lt n n) (eq nat n n)
 310 (refl_equal nat n)) (\lambda (m0: nat).(\lambda (H0: (le n m0)).(\lambda (_:
 311 (or (lt n m0) (eq nat n m0))).(or_introl (lt n (S m0)) (eq nat n (S m0))
 312 (le_n_S n m0 H0))))) m H))).
 313
 314 lemma le_or_lt:
 315  \forall (n: nat).(\forall (m: nat).(or (le n m) (lt m n)))
 316 \def
 317  \lambda (n: nat).(\lambda (m: nat).(nat_double_ind (\lambda (n0:
 318 nat).(\lambda (n1: nat).(or (le n0 n1) (lt n1 n0)))) (\lambda (n0:
 319 nat).(or_introl (le O n0) (lt n0 O) (le_O_n n0))) (\lambda (n0:
 320 nat).(or_intror (le (S n0) O) (lt O (S n0)) (lt_le_S O (S n0) (lt_O_Sn n0))))
 321 (\lambda (n0: nat).(\lambda (m0: nat).(\lambda (H: (or (le n0 m0) (lt m0
 322 n0))).(or_ind (le n0 m0) (lt m0 n0) (or (le (S n0) (S m0)) (lt (S m0) (S
 323 n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S
 324 n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S
 325 m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
 326
 327 lemma plus_n_O:
 328  \forall (n: nat).(eq nat n (plus n O))
 329 \def
 330  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (plus n0 O)))
 331 (refl_equal nat O) (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0
 332 O))).(f_equal nat nat S n0 (plus n0 O) H))) n).
 333
 334 lemma plus_n_Sm:
 335  \forall (n: nat).(\forall (m: nat).(eq nat (S (plus n m)) (plus n (S m))))
 336 \def
 337  \lambda (m: nat).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (S
 338 (plus n0 n)) (plus n0 (S n)))) (refl_equal nat (S n)) (\lambda (n0:
 339 nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S n)))).(f_equal nat nat
 340 S (S (plus n0 n)) (plus n0 (S n)) H))) m)).
 341
 342 lemma plus_sym:
 343  \forall (n: nat).(\forall (m: nat).(eq nat (plus n m) (plus m n)))
 344 \def
 345  \lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(eq nat (plus
 346 n0 m) (plus m n0))) (plus_n_O m) (\lambda (y: nat).(\lambda (H: (eq nat (plus
 347 y m) (plus m y))).(eq_ind nat (S (plus m y)) (\lambda (n0: nat).(eq nat (S
 348 (plus y m)) n0)) (f_equal nat nat S (plus y m) (plus m y) H) (plus m (S y))
 349 (plus_n_Sm m y)))) n)).
 350
 351 lemma plus_Snm_nSm:
 352  \forall (n: nat).(\forall (m: nat).(eq nat (plus (S n) m) (plus n (S m))))
 353 \def
 354  \lambda (n: nat).(\lambda (m: nat).(eq_ind_r nat (plus m n) (\lambda (n0:
 355 nat).(eq nat (S n0) (plus n (S m)))) (eq_ind_r nat (plus (S m) n) (\lambda
 356 (n0: nat).(eq nat (S (plus m n)) n0)) (refl_equal nat (plus (S m) n)) (plus n
 357 (S m)) (plus_sym n (S m))) (plus n m) (plus_sym n m))).
 358
 359 lemma plus_assoc_l:
 360  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus n (plus m
 361 p)) (plus (plus n m) p))))
 362 \def
 363  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 364 nat).(eq nat (plus n0 (plus m p)) (plus (plus n0 m) p))) (refl_equal nat
 365 (plus m p)) (\lambda (n0: nat).(\lambda (H: (eq nat (plus n0 (plus m p))
 366 (plus (plus n0 m) p))).(f_equal nat nat S (plus n0 (plus m p)) (plus (plus n0
 367 m) p) H))) n))).
 368
 369 lemma plus_assoc_r:
 370  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus (plus n
 371 m) p) (plus n (plus m p)))))
 372 \def
 373  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(sym_eq nat (plus n
 374 (plus m p)) (plus (plus n m) p) (plus_assoc_l n m p)))).
 375
 376 lemma simpl_plus_l:
 377  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus n m)
 378 (plus n p)) \to (eq nat m p))))
 379 \def
 380  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(\forall (p:
 381 nat).((eq nat (plus n0 m) (plus n0 p)) \to (eq nat m p))))) (\lambda (m:
 382 nat).(\lambda (p: nat).(\lambda (H: (eq nat m p)).H))) (\lambda (n0:
 383 nat).(\lambda (IHn: ((\forall (m: nat).(\forall (p: nat).((eq nat (plus n0 m)
 384 (plus n0 p)) \to (eq nat m p)))))).(\lambda (m: nat).(\lambda (p:
 385 nat).(\lambda (H: (eq nat (S (plus n0 m)) (S (plus n0 p)))).(IHn m p (IHn
 386 (plus n0 m) (plus n0 p) (f_equal nat nat (plus n0) (plus n0 m) (plus n0 p)
 387 (eq_add_S (plus n0 m) (plus n0 p) H))))))))) n).
 388
 389 lemma minus_n_O:
 390  \forall (n: nat).(eq nat n (minus n O))
 391 \def
 392  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (minus n0 O)))
 393 (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0
 394 O))).(refl_equal nat (S n0)))) n).
 395
 396 lemma minus_n_n:
 397  \forall (n: nat).(eq nat O (minus n n))
 398 \def
 399  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat O (minus n0 n0)))
 400 (refl_equal nat O) (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0
 401 n0))).IHn)) n).
 402
 403 lemma minus_Sn_m:
 404  \forall (n: nat).(\forall (m: nat).((le m n) \to (eq nat (S (minus n m))
 405 (minus (S n) m))))
 406 \def
 407  \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le m n)).(le_elim_rel
 408 (\lambda (n0: nat).(\lambda (n1: nat).(eq nat (S (minus n1 n0)) (minus (S n1)
 409 n0)))) (\lambda (p: nat).(f_equal nat nat S (minus p O) p (sym_eq nat p
 410 (minus p O) (minus_n_O p)))) (\lambda (p: nat).(\lambda (q: nat).(\lambda (_:
 411 (le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match p with [O \Rightarrow
 412 (S q) | (S l) \Rightarrow (minus q l)]))).H0)))) m n Le))).
 413
 414 lemma plus_minus:
 415  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat n (plus m p))
 416 \to (eq nat p (minus n m)))))
 417 \def
 418  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_double_ind
 419 (\lambda (n0: nat).(\lambda (n1: nat).((eq nat n1 (plus n0 p)) \to (eq nat p
 420 (minus n1 n0))))) (\lambda (n0: nat).(\lambda (H: (eq nat n0 p)).(eq_ind nat
 421 n0 (\lambda (n1: nat).(eq nat p n1)) (sym_eq nat n0 p H) (minus n0 O)
 422 (minus_n_O n0)))) (\lambda (n0: nat).(\lambda (H: (eq nat O (S (plus n0
 423 p)))).(False_ind (eq nat p O) (let H0 \def H in ((let H1 \def (O_S (plus n0
 424 p)) in (\lambda (H2: (eq nat O (S (plus n0 p)))).(H1 H2))) H0))))) (\lambda
 425 (n0: nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq
 426 nat p (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(H
 427 (eq_add_S m0 (plus n0 p) H0)))))) m n))).
 428
 429 lemma minus_plus:
 430  \forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
 431 \def
 432  \lambda (n: nat).(\lambda (m: nat).(sym_eq nat m (minus (plus n m) n)
 433 (plus_minus (plus n m) n m (refl_equal nat (plus n m))))).
 434
 435 lemma le_pred_n:
 436  \forall (n: nat).(le (pred n) n)
 437 \def
 438  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le (pred n0) n0)) (le_n O)
 439 (\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(le_S (pred (S n0)) n0
 440 (le_n n0)))) n).
 441
 442 lemma le_plus_l:
 443  \forall (n: nat).(\forall (m: nat).(le n (plus n m)))
 444 \def
 445  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(le n0 (plus
 446 n0 m)))) (\lambda (m: nat).(le_O_n m)) (\lambda (n0: nat).(\lambda (IHn:
 447 ((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(le_n_S n0 (plus
 448 n0 m) (IHn m))))) n).
 449
 450 lemma le_plus_r:
 451  \forall (n: nat).(\forall (m: nat).(le m (plus n m)))
 452 \def
 453  \lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(le m (plus
 454 n0 m))) (le_n m) (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(le_S m
 455 (plus n0 m) H))) n)).
 456
 457 lemma simpl_le_plus_l:
 458  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((le (plus p n) (plus p
 459 m)) \to (le n m))))
 460 \def
 461  \lambda (p: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (m:
 462 nat).((le (plus n n0) (plus n m)) \to (le n0 m))))) (\lambda (n:
 463 nat).(\lambda (m: nat).(\lambda (H: (le n m)).H))) (\lambda (p0:
 464 nat).(\lambda (IHp: ((\forall (n: nat).(\forall (m: nat).((le (plus p0 n)
 465 (plus p0 m)) \to (le n m)))))).(\lambda (n: nat).(\lambda (m: nat).(\lambda
 466 (H: (le (S (plus p0 n)) (S (plus p0 m)))).(IHp n m (le_S_n (plus p0 n) (plus
 467 p0 m) H))))))) p).
 468
 469 lemma le_plus_trans:
 470  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le n
 471 (plus m p)))))
 472 \def
 473  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n
 474 m)).(le_trans n m (plus m p) H (le_plus_l m p))))).
 475
 476 lemma le_reg_l:
 477  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le (plus
 478 p n) (plus p m)))))
 479 \def
 480  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 481 nat).((le n m) \to (le (plus n0 n) (plus n0 m)))) (\lambda (H: (le n m)).H)
 482 (\lambda (p0: nat).(\lambda (IHp: (((le n m) \to (le (plus p0 n) (plus p0
 483 m))))).(\lambda (H: (le n m)).(le_n_S (plus p0 n) (plus p0 m) (IHp H)))))
 484 p))).
 485
 486 lemma le_plus_plus:
 487  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
 488 n m) \to ((le p q) \to (le (plus n p) (plus m q)))))))
 489 \def
 490  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 491 nat).(\lambda (H: (le n m)).(\lambda (H0: (le p q)).(le_ind n (\lambda (n0:
 492 nat).(le (plus n p) (plus n0 q))) (le_reg_l p q n H0) (\lambda (m0:
 493 nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus m0 q))).(le_S
 494 (plus n p) (plus m0 q) H2)))) m H)))))).
 495
 496 lemma le_plus_minus:
 497  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus n (minus m
 498 n)))))
 499 \def
 500  \lambda (n: nat).(\lambda (m: nat).(\lambda (Le: (le n m)).(le_elim_rel
 501 (\lambda (n0: nat).(\lambda (n1: nat).(eq nat n1 (plus n0 (minus n1 n0)))))
 502 (\lambda (p: nat).(minus_n_O p)) (\lambda (p: nat).(\lambda (q: nat).(\lambda
 503 (_: (le p q)).(\lambda (H0: (eq nat q (plus p (minus q p)))).(f_equal nat nat
 504 S q (plus p (minus q p)) H0))))) n m Le))).
 505
 506 lemma le_plus_minus_r:
 507  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat (plus n (minus m
 508 n)) m)))
 509 \def
 510  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(sym_eq nat m
 511 (plus n (minus m n)) (le_plus_minus n m H)))).
 512
 513 lemma simpl_lt_plus_l:
 514  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt (plus p n) (plus p
 515 m)) \to (lt n m))))
 516 \def
 517  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 518 nat).((lt (plus n0 n) (plus n0 m)) \to (lt n m))) (\lambda (H: (lt n m)).H)
 519 (\lambda (p0: nat).(\lambda (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n
 520 m)))).(\lambda (H: (lt (S (plus p0 n)) (S (plus p0 m)))).(IHp (le_S_n (S
 521 (plus p0 n)) (plus p0 m) H))))) p))).
 522
 523 lemma lt_reg_l:
 524  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
 525 p n) (plus p m)))))
 526 \def
 527  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(nat_ind (\lambda (n0:
 528 nat).((lt n m) \to (lt (plus n0 n) (plus n0 m)))) (\lambda (H: (lt n m)).H)
 529 (\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to (lt (plus p0 n) (plus p0
 530 m))))).(\lambda (H: (lt n m)).(lt_n_S (plus p0 n) (plus p0 m) (IHp H)))))
 531 p))).
 532
 533 lemma lt_reg_r:
 534  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus
 535 n p) (plus m p)))))
 536 \def
 537  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (lt n
 538 m)).(eq_ind_r nat (plus p n) (\lambda (n0: nat).(lt n0 (plus m p))) (eq_ind_r
 539 nat (plus p m) (\lambda (n0: nat).(lt (plus p n) n0)) (nat_ind (\lambda (n0:
 540 nat).(lt (plus n0 n) (plus n0 m))) H (\lambda (n0: nat).(\lambda (_: (lt
 541 (plus n0 n) (plus n0 m))).(lt_reg_l n m (S n0) H))) p) (plus m p) (plus_sym m
 542 p)) (plus n p) (plus_sym n p))))).
 543
 544 lemma le_lt_plus_plus:
 545  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le
 546 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
 547 \def
 548  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 549 nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(eq_ind_r nat (plus n
 550 (S p)) (\lambda (n0: nat).(le n0 (plus m q))) (le_plus_plus n m (S p) q H H0)
 551 (plus (S n) p) (plus_Snm_nSm n p))))))).
 552
 553 lemma lt_le_plus_plus:
 554  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
 555 n m) \to ((le p q) \to (lt (plus n p) (plus m q)))))))
 556 \def
 557  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 558 nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(le_plus_plus (S n) m
 559 p q H H0)))))).
 560
 561 lemma lt_plus_plus:
 562  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt
 563 n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
 564 \def
 565  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q:
 566 nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(lt_le_plus_plus n m p q
 567 H (lt_le_weak p q H0))))))).
 568
 569 lemma well_founded_ltof:
 570  \forall (A: Type[0]).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
 571 \def
 572  \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n:
 573 nat).(nat_ind (\lambda (n0: nat).(\forall (a: A).((lt (f a) n0) \to (Acc A
 574 (ltof A f) a)))) (\lambda (a: A).(\lambda (H: (lt (f a) O)).(False_ind (Acc A
 575 (ltof A f) a) (let H0 \def H in ((let H1 \def (lt_n_O (f a)) in (\lambda (H2:
 576 (lt (f a) O)).(H1 H2))) H0))))) (\lambda (n0: nat).(\lambda (IHn: ((\forall
 577 (a: A).((lt (f a) n0) \to (Acc A (ltof A f) a))))).(\lambda (a: A).(\lambda
 578 (ltSma: (lt (f a) (S n0))).(Acc_intro A (ltof A f) a (\lambda (b: A).(\lambda
 579 (ltfafb: (lt (f b) (f a))).(IHn b (lt_le_trans (f b) (f a) n0 ltfafb
 580 (lt_n_Sm_le (f a) n0 ltSma)))))))))) n)) in (\lambda (a: A).(H (S (f a)) a
 581 (le_n (S (f a))))))).
 582
 583 lemma lt_wf:
 584  well_founded nat lt
 585 \def
 586  well_founded_ltof nat (\lambda (m: nat).m).
 587
 588 lemma lt_wf_ind:
 589  \forall (p: nat).(\forall (P: ((nat \to Prop))).(((\forall (n:
 590 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n)))) \to (P p)))
 591 \def
 592  \lambda (p: nat).(\lambda (P: ((nat \to Prop))).(\lambda (H: ((\forall (n:
 593 nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n))))).(Acc_ind nat lt
 594 (\lambda (n: nat).(P n)) (\lambda (x: nat).(\lambda (_: ((\forall (y:
 595 nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall (y: nat).((lt y
 596 x) \to (P y))))).(H x H1)))) p (lt_wf p)))).
 597