jHOLLight/Examples/ssrnat-compiled.hl

   1 needs "Examples/ssrbool-compiled.hl";;
   2
   3 (* Module Ssrnat*)
   4 module Ssrnat = struct
   5
   6 open Ssrbool;;
   7 overload_interface("+", `XOR`);;
   8 prioritize_num();;
   9
  10 (* Lemma succnK *)
  11 let succnK = Sections.section_proof ["n"]
  12 `SUC n - 1 = n`
  13 [
  14    ((arith_tac) THEN (done_tac));
  15 ];;
  16
  17 (* Lemma succn_inj *)
  18 let succn_inj = Sections.section_proof ["n";"m"]
  19 `SUC n = SUC m ==> n = m`
  20 [
  21    ((arith_tac) THEN (done_tac));
  22 ];;
  23
  24 (* Lemma eqSS *)
  25 let eqSS = Sections.section_proof ["m";"n"]
  26 `(SUC m = SUC n) = (m = n)`
  27 [
  28    ((arith_tac) THEN (done_tac));
  29 ];;
  30
  31 (* Lemma add0n *)
  32 let add0n = Sections.section_proof ["n"]
  33 `0 + n = n`
  34 [
  35    ((arith_tac) THEN (done_tac));
  36 ];;
  37
  38 (* Lemma addSn *)
  39 let addSn = Sections.section_proof ["m";"n"]
  40 `SUC m + n = SUC (m + n)`
  41 [
  42    ((arith_tac) THEN (done_tac));
  43 ];;
  44
  45 (* Lemma add1n *)
  46 let add1n = Sections.section_proof ["n"]
  47 `1 + n = SUC n`
  48 [
  49    ((arith_tac) THEN (done_tac));
  50 ];;
  51
  52 (* Lemma addn0 *)
  53 let addn0 = Sections.section_proof ["n"]
  54 `n + 0 = n`
  55 [
  56    ((arith_tac) THEN (done_tac));
  57 ];;
  58
  59 (* Lemma addnS *)
  60 let addnS = Sections.section_proof ["m";"n"]
  61 `m + SUC n = SUC (m + n)`
  62 [
  63    ((arith_tac) THEN (done_tac));
  64 ];;
  65
  66 (* Lemma addSnnS *)
  67 let addSnnS = Sections.section_proof ["m";"n"]
  68 `SUC m + n = m + SUC n`
  69 [
  70    ((arith_tac) THEN (done_tac));
  71 ];;
  72
  73 (* Lemma addnCA *)
  74 let addnCA = Sections.section_proof ["m";"n";"p"]
  75 `m + (n + p) = n + (m + p)`
  76 [
  77    ((arith_tac) THEN (done_tac));
  78 ];;
  79
  80 (* Lemma addnC *)
  81 let addnC = Sections.section_proof ["m";"n"]
  82 `m + n = n + m`
  83 [
  84    (((((fun arg_tac -> (use_arg_then2 ("addn0", [addn0])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("addnCA", [addnCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  85 ];;
  86
  87 (* Lemma addn1 *)
  88 let addn1 = Sections.section_proof ["n"]
  89 `n + 1 = SUC n`
  90 [
  91    (((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  92 ];;
  93
  94 (* Lemma addnA *)
  95 let addnA = Sections.section_proof ["n";"m";"p"]
  96 `n + (m + p) = (n + m) + p`
  97 [
  98    (((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [(`m + p`)])))) THEN (((use_arg_then2 ("addnCA", [addnCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  99 ];;
 100
 101 (* Lemma addnAC *)
 102 let addnAC = Sections.section_proof ["m";"n";"p"]
 103 `(n + m) + p = (n + p) + m`
 104 [
 105    (((repeat_tactic 1 9 (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [(`p + m`)]))))) THEN (done_tac));
 106 ];;
 107
 108 (* Lemma addn_eq0 *)
 109 let addn_eq0 = Sections.section_proof ["m";"n"]
 110 `(m + n = 0) <=> (m = 0) /\ (n = 0)`
 111 [
 112    ((arith_tac) THEN (done_tac));
 113 ];;
 114
 115 (* Lemma eqn_addl *)
 116 let eqn_addl = Sections.section_proof ["p";"m";"n"]
 117 `(p + m = p + n) <=> (m = n)`
 118 [
 119    ((arith_tac) THEN (done_tac));
 120 ];;
 121
 122 (* Lemma eqn_addr *)
 123 let eqn_addr = Sections.section_proof ["p";"m";"n"]
 124 `(m + p = n + p) = (m = n)`
 125 [
 126    ((arith_tac) THEN (done_tac));
 127 ];;
 128
 129 (* Lemma addnI *)
 130 let addnI = Sections.section_proof ["m";"n1";"n2"]
 131 `m + n1 = m + n2 ==> n1 = n2`
 132 [
 133    ((BETA_TAC THEN (move ["Heq"])) THEN (((fun arg_tac -> (use_arg_then2 ("eqn_addl", [eqn_addl])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 134 ];;
 135
 136 (* Lemma addIn *)
 137 let addIn = Sections.section_proof ["m";"n1";"n2"]
 138 `n1 + m = n2 + m ==> n1 = n2`
 139 [
 140    ((repeat_tactic 1 9 (((use_arg_then2 ("addnC", [addnC]))(gsym_then (thm_tac (new_rewrite [] [(`_1 + m`)])))))) THEN (move ["Heq"]));
 141    ((((fun arg_tac -> (use_arg_then2 ("addnI", [addnI])) (fun fst_arg -> (use_arg_then2 ("Heq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
 142 ];;
 143
 144 (* Lemma sub0n *)
 145 let sub0n = Sections.section_proof ["n"]
 146 `0 - n = 0`
 147 [
 148    ((arith_tac) THEN (done_tac));
 149 ];;
 150
 151 (* Lemma subn0 *)
 152 let subn0 = Sections.section_proof ["n"]
 153 `n - 0 = n`
 154 [
 155    ((arith_tac) THEN (done_tac));
 156 ];;
 157
 158 (* Lemma subnn *)
 159 let subnn = Sections.section_proof []
 160 `!n. n - n = 0`
 161 [
 162    ((arith_tac) THEN (done_tac));
 163 ];;
 164
 165 (* Lemma subSS *)
 166 let subSS = Sections.section_proof []
 167 `!n m. SUC m - SUC n = m - n`
 168 [
 169    ((arith_tac) THEN (done_tac));
 170 ];;
 171
 172 (* Lemma subn_add2l *)
 173 let subn_add2l = Sections.section_proof []
 174 `!p m n. (p + m) - (p + n) = m - n`
 175 [
 176    ((arith_tac) THEN (done_tac));
 177 ];;
 178
 179 (* Lemma subn_add2r *)
 180 let subn_add2r = Sections.section_proof []
 181 `!p m n. (m + p) - (n + p) = m - n`
 182 [
 183    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 184    (((repeat_tactic 1 9 (((use_arg_then2 ("addnC", [addnC]))(gsym_then (thm_tac (new_rewrite [] [(`_1 + p`)])))))) THEN (((use_arg_then2 ("subn_add2l", [subn_add2l]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 185 ];;
 186
 187 (* Lemma addKn *)
 188 let addKn = Sections.section_proof ["n"]
 189 `!x. (n + x) - n = x`
 190 [
 191    ((BETA_TAC THEN (move ["m"])) THEN ((((use_arg_then2 ("addn0", [addn0]))(gsym_then (thm_tac (new_rewrite [2] [(`n`)]))))) THEN (((use_arg_then2 ("subn_add2l", [subn_add2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subn0", [subn0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 192 ];;
 193
 194 (* Lemma addnK *)
 195 let addnK = Sections.section_proof []
 196 `!n x. (x + n) - n = x`
 197 [
 198    ((BETA_TAC THEN (move ["n"]) THEN (move ["m"])) THEN ((((fun arg_tac -> (use_arg_then2 ("addnC", [addnC])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addKn", [addKn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 199 ];;
 200
 201 (* Lemma subSnn *)
 202 let subSnn = Sections.section_proof ["n"]
 203 `SUC n - n = 1`
 204 [
 205    (((((use_arg_then2 ("add1n", [add1n]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnK", [addnK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 206 ];;
 207
 208 (* Lemma subn_sub *)
 209 let subn_sub = Sections.section_proof ["m";"n";"p"]
 210 `(n - m) - p = n - (m + p)`
 211 [
 212    ((arith_tac) THEN (done_tac));
 213 ];;
 214
 215 (* Lemma subnAC *)
 216 let subnAC = Sections.section_proof []
 217 `!m n p. (m - n) - p = (m - p) - n`
 218 [
 219    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("subn_sub", [subn_sub]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 220 ];;
 221
 222 (* Lemma predn_sub *)
 223 let predn_sub = Sections.section_proof []
 224 `!m n. (m - n) - 1 = m - SUC n`
 225 [
 226    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN ((((use_arg_then2 ("subn_sub", [subn_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn1", [addn1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 227 ];;
 228
 229 (* Lemma predn_subS *)
 230 let predn_subS = Sections.section_proof []
 231 `!m n. (SUC m - n) - 1 = m - n`
 232 [
 233    (((((use_arg_then2 ("predn_sub", [predn_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subSS", [subSS]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 234 ];;
 235
 236 (* Lemma ltnS *)
 237 let ltnS = Sections.section_proof []
 238 `!m n. (m < SUC n) = (m <= n)`
 239 [
 240    ((arith_tac) THEN (done_tac));
 241 ];;
 242
 243 (* Lemma leq0n *)
 244 let leq0n = Sections.section_proof []
 245 `!n. 0 <= n`
 246 [
 247    ((arith_tac) THEN (done_tac));
 248 ];;
 249
 250 (* Lemma ltn0Sn *)
 251 let ltn0Sn = Sections.section_proof []
 252 `!n. 0 < SUC n`
 253 [
 254    ((arith_tac) THEN (done_tac));
 255 ];;
 256
 257 (* Lemma ltn0 *)
 258 let ltn0 = Sections.section_proof []
 259 `!n. n < 0 <=> F`
 260 [
 261    ((arith_tac) THEN (done_tac));
 262 ];;
 263
 264 (* Lemma leqnn *)
 265 let leqnn = Sections.section_proof []
 266 `!n. n <= n`
 267 [
 268    ((arith_tac) THEN (done_tac));
 269 ];;
 270
 271 (* Lemma ltnSn *)
 272 let ltnSn = Sections.section_proof []
 273 `!n. n < SUC n`
 274 [
 275    ((arith_tac) THEN (done_tac));
 276 ];;
 277
 278 (* Lemma eq_leq *)
 279 let eq_leq = Sections.section_proof []
 280 `!m n. m = n ==> m <= n`
 281 [
 282    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 283 ];;
 284
 285 (* Lemma leqnSn *)
 286 let leqnSn = Sections.section_proof []
 287 `!n. n <= SUC n`
 288 [
 289    ((arith_tac) THEN (done_tac));
 290 ];;
 291
 292 (* Lemma leq_pred *)
 293 let leq_pred = Sections.section_proof []
 294 `!n. n - 1 <= n`
 295 [
 296    ((arith_tac) THEN (done_tac));
 297 ];;
 298
 299 (* Lemma leqSpred *)
 300 let leqSpred = Sections.section_proof []
 301 `!n. n <= SUC (n - 1)`
 302 [
 303    ((arith_tac) THEN (done_tac));
 304 ];;
 305
 306 (* Lemma ltn_predK *)
 307 let ltn_predK = Sections.section_proof []
 308 `!m n. m < n ==> SUC (n - 1) = n`
 309 [
 310    ((arith_tac) THEN (done_tac));
 311 ];;
 312
 313 (* Lemma prednK *)
 314 let prednK = Sections.section_proof []
 315 `!n. 0 < n ==> SUC (n - 1) = n`
 316 [
 317    ((BETA_TAC THEN (move ["n"]) THEN (move ["H"])) THEN (((fun arg_tac -> (use_arg_then2 ("ltn_predK", [ltn_predK])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac)));
 318 ];;
 319
 320 (* Lemma leqNgt *)
 321 let leqNgt = Sections.section_proof []
 322 `!m n. (m <= n) <=> ~(n < m)`
 323 [
 324    ((arith_tac) THEN (done_tac));
 325 ];;
 326
 327 (* Lemma ltnNge *)
 328 let ltnNge = Sections.section_proof []
 329 `!m n. (m < n) = ~(n <= m)`
 330 [
 331    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 332 ];;
 333
 334 (* Lemma ltnn *)
 335 let ltnn = Sections.section_proof []
 336 `!n. n < n <=> F`
 337 [
 338    ((BETA_TAC THEN (move ["n"])) THEN ((((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 339 ];;
 340
 341 (* Lemma leqn0 *)
 342 let leqn0 = Sections.section_proof []
 343 `!n. (n <= 0) = (n = 0)`
 344 [
 345    ((arith_tac) THEN (done_tac));
 346 ];;
 347
 348 (* Lemma lt0n *)
 349 let lt0n = Sections.section_proof []
 350 `!n. (0 < n) = ~(n = 0)`
 351 [
 352    ((arith_tac) THEN (done_tac));
 353 ];;
 354
 355 (* Lemma lt0n_neq0 *)
 356 let lt0n_neq0 = Sections.section_proof []
 357 `!n. 0 < n ==> ~(n = 0)`
 358 [
 359    ((arith_tac) THEN (done_tac));
 360 ];;
 361
 362 (* Lemma eqn0Ngt *)
 363 let eqn0Ngt = Sections.section_proof []
 364 `!n. (n = 0) = ~(0 < n)`
 365 [
 366    ((arith_tac) THEN (done_tac));
 367 ];;
 368
 369 (* Lemma neq0_lt0n *)
 370 let neq0_lt0n = Sections.section_proof []
 371 `!n. (n = 0) = F ==> 0 < n`
 372 [
 373    ((arith_tac) THEN (done_tac));
 374 ];;
 375
 376 (* Lemma eqn_leq *)
 377 let eqn_leq = Sections.section_proof []
 378 `!m n. (m = n) = (m <= n /\ n <= m)`
 379 [
 380    ((arith_tac) THEN (done_tac));
 381 ];;
 382
 383 (* Lemma anti_leq *)
 384 let anti_leq = Sections.section_proof []
 385 `!m n. m <= n /\ n <= m ==> m = n`
 386 [
 387    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then2 ("eqn_leq", [eqn_leq]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 388 ];;
 389
 390 (* Lemma neq_ltn *)
 391 let neq_ltn = Sections.section_proof []
 392 `!m n. ~(m = n) <=> (m < n) \/ (n < m)`
 393 [
 394    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 395    (((((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbC", [orbC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 396 ];;
 397
 398 (* Lemma leq_eqVlt *)
 399 let leq_eqVlt = Sections.section_proof ["m";"n"]
 400 `(m <= n) <=> (m = n) \/ (m < n)`
 401 [
 402    ((arith_tac) THEN (done_tac));
 403 ];;
 404
 405 (* Lemma eq_sym *)
 406 let eq_sym = Sections.section_proof []
 407 `!x y:A. x = y <=> y = x`
 408 [
 409    ((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ])) (disch_tac [])) THEN (clear_assumption "EQ_SYM_EQ") THEN BETA_TAC) THEN (done_tac));
 410 ];;
 411
 412 (* Lemma ltn_neqAle *)
 413 let ltn_neqAle = Sections.section_proof []
 414 `!m n. (m < n) <=> ~(m = n) /\ (m <= n)`
 415 [
 416    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 417    (((((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_eqVlt", [leq_eqVlt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [(`n = m`)]))))) THEN (done_tac));
 418 ];;
 419
 420 (* Lemma leq_trans *)
 421 let leq_trans = Sections.section_proof []
 422 `!n m p. m <= n ==> n <= p ==> m <= p`
 423 [
 424    ((arith_tac) THEN (done_tac));
 425 ];;
 426
 427 (* Lemma ltE *)
 428 let ltE = Sections.section_proof []
 429 `!n m. n < m <=> SUC n <= m`
 430 [
 431    ((arith_tac) THEN (done_tac));
 432 ];;
 433
 434 (* Lemma leqSS *)
 435 let leqSS = Sections.section_proof []
 436 `!n m. SUC n <= SUC m <=> n <= m`
 437 [
 438    ((arith_tac) THEN (done_tac));
 439 ];;
 440
 441 (* Lemma leq_ltn_trans *)
 442 let leq_ltn_trans = Sections.section_proof []
 443 `!n m p. m <= n ==> n < p ==> m < p`
 444 [
 445    (BETA_TAC THEN (move ["n"]) THEN (move ["m"]) THEN (move ["p"]) THEN (move ["Hmn"]));
 446    (((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_trans", [leq_trans])) (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("leqSS", [leqSS]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)) THEN (done_tac));
 447 ];;
 448
 449 (* Lemma ltn_leq_trans *)
 450 let ltn_leq_trans = Sections.section_proof ["n";"m";"p"]
 451 `m < n ==> n <= p ==> m < p`
 452 [
 453    ((arith_tac) THEN (done_tac));
 454 ];;
 455
 456 (* Lemma ltnW *)
 457 let ltnW = Sections.section_proof []
 458 `!m n. m < n ==> m <= n`
 459 [
 460    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_trans", [leq_trans])) (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("leqnSn", [leqnSn]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 461 ];;
 462
 463 (* Lemma leqW *)
 464 let leqW = Sections.section_proof []
 465 `!m n. m <= n ==> m <= SUC n`
 466 [
 467    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["le_mn"])) THEN (((use_arg_then2 ("ltnW", [ltnW])) (disch_tac [])) THEN (clear_assumption "ltnW") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqSS", [leqSS]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 468 ];;
 469
 470 (* Lemma ltn_trans *)
 471 let ltn_trans = Sections.section_proof []
 472 `!n m p. m < n ==> n < p ==> m < p`
 473 [
 474    (BETA_TAC THEN (move ["n"]) THEN (move ["m"]) THEN (move ["p"]) THEN (move ["lt_mn"]));
 475    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("ltnW", [ltnW])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))));
 476    ((((use_arg_then2 ("leq_trans", [leq_trans])) (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 477 ];;
 478
 479 (* Lemma geqE *)
 480 let geqE = Sections.section_proof []
 481 `!m n. m >= n <=> n <= m`
 482 [
 483    ((arith_tac) THEN (done_tac));
 484 ];;
 485
 486 (* Lemma gtE *)
 487 let gtE = Sections.section_proof ["m";"n"]
 488 `m > n <=> n < m`
 489 [
 490    (arith_tac);
 491 ];;
 492
 493 (* Lemma leq_total *)
 494 let leq_total = Sections.section_proof ["m";"n"]
 495 `(m <= n) \/ (n <= m)`
 496 [
 497    ((((((use_arg_then2 ("implyNb", [implyNb]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ltnNge", [ltnNge]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["lt_nm"])) THEN (((use_arg_then2 ("ltnW", [ltnW])) (disch_tac [])) THEN (clear_assumption "ltnW") THEN (exact_tac)) THEN (done_tac));
 498 ];;
 499
 500 (* Lemma leqP *)
 501 let leqP = Sections.section_proof ["m";"n"]
 502 `m <= n \/ n < m`
 503 [
 504    ((arith_tac) THEN (done_tac));
 505 ];;
 506
 507 (* Lemma ltnP *)
 508 let ltnP = Sections.section_proof ["m";"n"]
 509 `m < n \/ n <= m`
 510 [
 511    ((arith_tac) THEN (done_tac));
 512 ];;
 513
 514 (* Lemma posnP *)
 515 let posnP = Sections.section_proof ["n"]
 516 `n = 0 \/ 0 < n`
 517 [
 518    ((arith_tac) THEN (done_tac));
 519 ];;
 520
 521 (* Lemma ltngtP *)
 522 let ltngtP = Sections.section_proof ["m";"n"]
 523 `m < n \/ n < m \/ m = n`
 524 [
 525    ((arith_tac) THEN (done_tac));
 526 ];;
 527
 528 (* Lemma leq_add2l *)
 529 let leq_add2l = Sections.section_proof []
 530 `!p m n. (p + m <= p + n) = (m <= n)`
 531 [
 532    ((arith_tac) THEN (done_tac));
 533 ];;
 534
 535 (* Lemma ltn_add2l *)
 536 let ltn_add2l = Sections.section_proof []
 537 `!p m n. (p + m < p + n) = (m < n)`
 538 [
 539    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 540    (((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnS", [addnS]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_add2l", [leq_add2l]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 541 ];;
 542
 543 (* Lemma leq_add2r *)
 544 let leq_add2r = Sections.section_proof ["p";"m";"n"]
 545 `(m + p <= n + p) = (m <= n)`
 546 [
 547    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("addnC", [addnC])) (fun fst_arg -> (use_arg_then2 ("p", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("leq_add2l", [leq_add2l]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 548 ];;
 549
 550 (* Lemma ltn_add2r *)
 551 let ltn_add2r = Sections.section_proof []
 552 `!p m n. (m + p < n + p) = (m < n)`
 553 [
 554    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 555    (((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addSn", [addSn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_add2r", [leq_add2r]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 556 ];;
 557
 558 (* Lemma leq_add *)
 559 let leq_add = Sections.section_proof []
 560 `!m1 m2 n1 n2. m1 <= n1 ==> m2 <= n2 ==> m1 + m2 <= n1 + n2`
 561 [
 562    (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n1"]) THEN (move ["n2"]) THEN (move ["le_mn1"]) THEN (move ["le_mn2"]));
 563    (((((fun arg_tac -> (use_arg_then2 ("leq_trans", [leq_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 + n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_add2l", [leq_add2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_add2r", [leq_add2r]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 564 ];;
 565
 566 (* Lemma leq_addr *)
 567 let leq_addr = Sections.section_proof []
 568 `!m n. n <= n + m`
 569 [
 570    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 571    (((((use_arg_then2 ("addn0", [addn0]))(gsym_then (thm_tac (new_rewrite [1] [(`n`)]))))) THEN (((use_arg_then2 ("leq_add2l", [leq_add2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq0n", [leq0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 572 ];;
 573
 574 (* Lemma leq_addl *)
 575 let leq_addl = Sections.section_proof []
 576 `!m n. n <= m + n`
 577 [
 578    (((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_addr", [leq_addr]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 579 ];;
 580
 581 (* Lemma ltn_addr *)
 582 let ltn_addr = Sections.section_proof ["m";"n";"p"]
 583 `m < n ==> m < n + p`
 584 [
 585    ((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("leq_trans", [leq_trans])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_addr", [leq_addr]))(thm_tac (new_rewrite [] [])))));
 586 ];;
 587
 588 (* Lemma ltn_addl *)
 589 let ltn_addl = Sections.section_proof []
 590 `!m n p. m < n ==> m < p + n`
 591 [
 592    ((arith_tac) THEN (done_tac));
 593 ];;
 594
 595 (* Lemma addn_gt0 *)
 596 let addn_gt0 = Sections.section_proof []
 597 `!m n. (0 < m + n) <=> (0 < m) \/ (0 < n)`
 598 [
 599    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 600    (((repeat_tactic 1 9 (((use_arg_then2 ("lt0n", [lt0n]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addn_eq0", [addn_eq0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 601 ];;
 602
 603 (* Lemma subn_gt0 *)
 604 let subn_gt0 = Sections.section_proof ["m";"n"]
 605 `(0 < n - m) = (m < n)`
 606 [
 607    ((arith_tac) THEN (done_tac));
 608 ];;
 609
 610 (* Lemma subn_eq0 *)
 611 let subn_eq0 = Sections.section_proof []
 612 `!m n. (m - n = 0) = (m <= n)`
 613 [
 614    ((arith_tac) THEN (done_tac));
 615 ];;
 616
 617 (* Lemma leqE *)
 618 let leqE = Sections.section_proof []
 619 `!m n. m <= n <=> m - n = 0`
 620 [
 621    ((arith_tac) THEN (done_tac));
 622 ];;
 623
 624 (* Lemma leq_sub_add *)
 625 let leq_sub_add = Sections.section_proof []
 626 `!m n p. (m - n <= p) = (m <= n + p)`
 627 [
 628    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 629    (((((use_arg_then2 ("subn_eq0", [subn_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subn_sub", [subn_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqE", [leqE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 630 ];;
 631
 632 (* Lemma leq_subr *)
 633 let leq_subr = Sections.section_proof []
 634 `!m n. n - m <= n`
 635 [
 636    (((((use_arg_then2 ("leq_sub_add", [leq_sub_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_addl", [leq_addl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 637 ];;
 638
 639 (* Lemma subnKC *)
 640 let subnKC = Sections.section_proof []
 641 `!m n. m <= n ==> m + (n - m) = n`
 642 [
 643    ((arith_tac) THEN (done_tac));
 644 ];;
 645
 646 (* Lemma subnK *)
 647 let subnK = Sections.section_proof []
 648 `!m n. m <= n ==> (n - m) + m = n`
 649 [
 650    ((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subnKC", [subnKC])) (disch_tac [])) THEN (clear_assumption "subnKC") THEN (exact_tac)) THEN (done_tac));
 651 ];;
 652
 653 (* Lemma addn_subA *)
 654 let addn_subA = Sections.section_proof []
 655 `!m n p. p <= n ==> m + (n - p) = (m + n) - p`
 656 [
 657    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]) THEN (move ["le_pn"]));
 658    (((((fun arg_tac -> (use_arg_then2 ("subnK", [subnK])) (fun fst_arg -> (use_arg_then2 ("le_pn", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("addnA", [addnA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnK", [addnK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 659 ];;
 660
 661 (* Lemma subn_subA *)
 662 let subn_subA = Sections.section_proof []
 663 `!m n p. p <= n ==> m - (n - p) = (m + p) - n`
 664 [
 665    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]) THEN (move ["le_pn"]));
 666    (((((fun arg_tac -> (use_arg_then2 ("subnK", [subnK])) (fun fst_arg -> (use_arg_then2 ("le_pn", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("subn_add2r", [subn_add2r]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 667 ];;
 668
 669 (* Lemma subKn *)
 670 let subKn = Sections.section_proof []
 671 `!m n. m <= n ==> n - (n - m) = m`
 672 [
 673    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 674    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("subn_subA", [subn_subA])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addKn", [addKn]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 675 ];;
 676
 677 (* Lemma leq_subS *)
 678 let leq_subS = Sections.section_proof []
 679 `!m n. m <= n ==> SUC n - m = SUC (n - m)`
 680 [
 681    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 682    ((((use_arg_then2 ("add1n", [add1n]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("addn_subA", [addn_subA])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))));
 683    ((((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 684 ];;
 685
 686 (* Lemma ltn_subS *)
 687 let ltn_subS = Sections.section_proof []
 688 `!m n. m < n ==> n - m = SUC (n - SUC m)`
 689 [
 690    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["lt_mn"])) THEN ((((use_arg_then2 ("leq_subS", [leq_subS]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("subSS", [subSS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 691 ];;
 692
 693 (* Lemma leq_sub2r *)
 694 let leq_sub2r = Sections.section_proof []
 695 `!p m n. m <= n ==> m - p <= n - p`
 696 [
 697    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]) THEN (move ["le_mn"]));
 698    (((((use_arg_then2 ("leq_sub_add", [leq_sub_add]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("leq_trans", [leq_trans])) (fun fst_arg -> (use_arg_then2 ("le_mn", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_sub_add", [leq_sub_add]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 699 ];;
 700
 701 (* Lemma leq_sub2l *)
 702 let leq_sub2l = Sections.section_proof []
 703 `!p m n. m <= n ==> p - n <= p - m`
 704 [
 705    ((BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])) THEN ((((fun arg_tac -> (use_arg_then2 ("leq_add2r", [leq_add2r])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`p - m`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_sub_add", [leq_sub_add]))(thm_tac (new_rewrite [] []))))));
 706    ((((use_arg_then2 ("leq_trans", [leq_trans])) (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("leq_sub_add", [leq_sub_add]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 707 ];;
 708
 709 (* Lemma leq_sub2 *)
 710 let leq_sub2 = Sections.section_proof []
 711 `!m1 m2 n1 n2. m1 <= m2 ==> n2 <= n1 ==> m1 - n1 <= m2 - n2`
 712 [
 713    (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n1"]) THEN (move ["n2"]));
 714    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("leq_sub2r", [leq_sub2r])) (fun fst_arg -> (use_arg_then2 ("n1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["le_m12"])) THEN ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("leq_sub2l", [leq_sub2l])) (fun fst_arg -> (use_arg_then2 ("m2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then2 ("leq_trans", [leq_trans])) (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (exact_tac)));
 715 ];;
 716
 717 (* Lemma ltn_sub2r *)
 718 let ltn_sub2r = Sections.section_proof []
 719 `!p m n. p < n ==> m < n ==> m - p < n - p`
 720 [
 721    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 722    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("ltn_subS", [ltn_subS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leqSS", [leqSS]))(thm_tac (new_rewrite [] []))))));
 723    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("leq_sub2r", [leq_sub2r])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SUC p`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then2 ("subSS", [subSS]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 724 ];;
 725
 726 (* Lemma ltn_sub2l *)
 727 let ltn_sub2l = Sections.section_proof []
 728 `!p m n. m < p ==> m < n ==> p - n < p - m`
 729 [
 730    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 731    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("ltn_subS", [ltn_subS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leqSS", [leqSS]))(thm_tac (new_rewrite [] []))))));
 732    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("leq_sub2l", [leq_sub2l])) (fun fst_arg -> (use_arg_then2 ("p", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (done_tac));
 733 ];;
 734
 735 (* Lemma ltn_add_sub *)
 736 let ltn_add_sub = Sections.section_proof []
 737 `!m n p. (m + n < p) = (n < p - m)`
 738 [
 739    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 740    (((repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_sub_add", [leq_sub_add]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 741 ];;
 742 let maxn = new_definition `maxn m n = if m < n then n else m`;;
 743 let minn = new_definition `minn m n = if m < n then m else n`;;
 744
 745 (* Lemma max0n *)
 746 let max0n = Sections.section_proof []
 747 `!n. maxn 0 n = n`
 748 [
 749    ((((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 750 ];;
 751
 752 (* Lemma maxn0 *)
 753 let maxn0 = Sections.section_proof []
 754 `!n. maxn n 0 = n`
 755 [
 756    ((((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 757 ];;
 758
 759 (* Lemma maxnC *)
 760 let maxnC = Sections.section_proof []
 761 `!m n. maxn m n = maxn n m`
 762 [
 763    ((repeat_tactic 1 9 (((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
 764 ];;
 765
 766 (* Lemma maxnl *)
 767 let maxnl = Sections.section_proof []
 768 `!m n. n <= m ==> maxn m n = m`
 769 [
 770    ((((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 771 ];;
 772
 773 (* Lemma maxnr *)
 774 let maxnr = Sections.section_proof []
 775 `!m n. m <= n ==> maxn m n = n`
 776 [
 777    ((((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 778 ];;
 779
 780 (* Lemma add_sub_maxn *)
 781 let add_sub_maxn = Sections.section_proof []
 782 `!m n. m + (n - m) = maxn m n`
 783 [
 784    ((((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 785 ];;
 786
 787 (* Lemma maxnAC *)
 788 let maxnAC = Sections.section_proof []
 789 `!m n p. maxn (maxn m n) p = maxn (maxn m p) n`
 790 [
 791    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 792    (((repeat_tactic 1 9 (((use_arg_then2 ("add_sub_maxn", [add_sub_maxn]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("subn_sub", [subn_sub]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("add_sub_maxn", [add_sub_maxn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 793 ];;
 794
 795 (* Lemma maxnA *)
 796 let maxnA = Sections.section_proof []
 797 `!m n p. maxn m (maxn n p) = maxn (maxn m n) p`
 798 [
 799    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 800    (((repeat_tactic 1 9 (((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (((use_arg_then2 ("maxnAC", [maxnAC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 801 ];;
 802
 803 (* Lemma maxnCA *)
 804 let maxnCA = Sections.section_proof []
 805 `!m n p. maxn m (maxn n p) = maxn n (maxn m p)`
 806 [
 807    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("maxnA", [maxnA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (done_tac));
 808 ];;
 809
 810 (* Lemma eqn_maxr *)
 811 let eqn_maxr = Sections.section_proof []
 812 `!m n. (maxn m n = n) = (m <= n)`
 813 [
 814    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 815    (((((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn0", [addn0]))(gsym_then (thm_tac (new_rewrite [2] [(`n`)]))))) THEN (((use_arg_then2 ("add_sub_maxn", [add_sub_maxn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqn_addl", [eqn_addl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqE", [leqE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 816 ];;
 817
 818 (* Lemma eqn_maxl *)
 819 let eqn_maxl = Sections.section_proof []
 820 `!m n. (maxn m n = m) = (n <= m)`
 821 [
 822    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 823    (((((use_arg_then2 ("addn0", [addn0]))(gsym_then (thm_tac (new_rewrite [2] [(`m`)]))))) THEN (((use_arg_then2 ("add_sub_maxn", [add_sub_maxn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqn_addl", [eqn_addl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqE", [leqE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 824 ];;
 825
 826 (* Lemma maxnn *)
 827 let maxnn = Sections.section_proof []
 828 `!n. maxn n n = n`
 829 [
 830    (BETA_TAC THEN (move ["n"]));
 831    (((((use_arg_then2 ("maxnl", [maxnl]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 832 ];;
 833
 834 (* Lemma leq_maxr *)
 835 let leq_maxr = Sections.section_proof ["m";"n1";"n2"]
 836 `(m <= maxn n1 n2) <=> (m <= n1) \/ (m <= n2)`
 837 [
 838    ((fun arg_tac -> arg_tac (Arg_term (`n2 <= n1`))) (term_tac (wlog_tac (move ["le_n21"])[`n1`; `n2`])));
 839    (((THENL_LAST) (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leq_total", [leq_total])) (fun fst_arg -> (use_arg_then2 ("n2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (move ["le_n12"])) ((((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbC", [orbC]))(thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("le_n21", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 840    (BETA_TAC THEN (move ["le_n21"]));
 841    (((((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("le_n21", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("EXCLUDED_MIDDLE", [EXCLUDED_MIDDLE])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m <= n1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (simp_tac)));
 842    ((((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("leq_trans", [leq_trans])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN ((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("n1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac));
 843 ];;
 844
 845 (* Lemma leq_maxl *)
 846 let leq_maxl = Sections.section_proof ["m";"n1";"n2"]
 847 `(maxn n1 n2 <= m) <=> (n1 <= m) /\ (n2 <= m)`
 848 [
 849    (((((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_maxr", [leq_maxr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leqNgt", [leqNgt]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 850 ];;
 851
 852 (* Lemma addn_maxl *)
 853 let addn_maxl = Sections.section_proof []
 854 `!m1 m2 n. (maxn m1 m2) + n = maxn (m1 + n) (m2 + n)`
 855 [
 856    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("add_sub_maxn", [add_sub_maxn]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("subn_add2r", [subn_add2r]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnAC", [addnAC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 857 ];;
 858
 859 (* Lemma addn_maxr *)
 860 let addn_maxr = Sections.section_proof []
 861 `!m n1 n2. m + maxn n1 n2 = maxn (m + n1) (m + n2)`
 862 [
 863    ((BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [(`m + _1`)]))))) THEN (((use_arg_then2 ("addn_maxl", [addn_maxl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 864 ];;
 865
 866 (* Lemma min0n *)
 867 let min0n = Sections.section_proof ["n"]
 868 `minn 0 n = 0`
 869 [
 870    ((((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 871 ];;
 872
 873 (* Lemma minn0 *)
 874 let minn0 = Sections.section_proof ["n"]
 875 `minn n 0 = 0`
 876 [
 877    ((((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 878 ];;
 879
 880 (* Lemma minnC *)
 881 let minnC = Sections.section_proof ["m";"n"]
 882 `minn m n = minn n m`
 883 [
 884    ((repeat_tactic 1 9 (((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
 885 ];;
 886
 887 (* Lemma minnr *)
 888 let minnr = Sections.section_proof ["m";"n"]
 889 `n <= m ==> minn m n = n`
 890 [
 891    ((((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 892 ];;
 893
 894 (* Lemma minnl *)
 895 let minnl = Sections.section_proof ["m";"n"]
 896 `m <= n ==> minn m n = m`
 897 [
 898    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("minnr", [minnr])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 899 ];;
 900
 901 (* Lemma addn_min_max *)
 902 let addn_min_max = Sections.section_proof ["m";"n"]
 903 `minn m n + maxn m n = m + n`
 904 [
 905    (((((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
 906 ];;
 907
 908 (* Lemma minn_to_maxn *)
 909 let minn_to_maxn = Sections.section_proof ["m";"n"]
 910 `minn m n = (m + n) - maxn m n`
 911 [
 912    (((((use_arg_then2 ("addn_min_max", [addn_min_max]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnK", [addnK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 913 ];;
 914
 915 (* Lemma sub_sub_minn *)
 916 let sub_sub_minn = Sections.section_proof ["m";"n"]
 917 `m - (m - n) = minn m n`
 918 [
 919    (((((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("minn_to_maxn", [minn_to_maxn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add_sub_maxn", [add_sub_maxn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subn_add2l", [subn_add2l]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 920 ];;
 921
 922 (* Lemma minnCA *)
 923 let minnCA = Sections.section_proof []
 924 `!m1 m2 m3. minn m1 (minn m2 m3) = minn m2 (minn m1 m3)`
 925 [
 926    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["m3"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("minn_to_maxn", [minn_to_maxn]))(thm_tac (new_rewrite [] [(`minn _1 (minn _2 _3)`)]))))));
 927    ((((fun arg_tac -> (use_arg_then2 ("subn_add2r", [subn_add2r])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`maxn m2 m3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("subn_add2r", [subn_add2r])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`maxn m1 m3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`(m2 + _1) - _2`)]))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] [])))))));
 928    (((repeat_tactic 1 9 (((use_arg_then2 ("addn_maxl", [addn_maxl]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addn_min_max", [addn_min_max]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addn_maxr", [addn_maxr]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnCA", [addnCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("maxnAC", [maxnAC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [(`m2 + m1`)]))))) THEN (done_tac));
 929 ];;
 930
 931 (* Lemma minnA *)
 932 let minnA = Sections.section_proof []
 933 `!m1 m2 m3. minn m1 (minn m2 m3) = minn (minn m1 m2) m3`
 934 [
 935    (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["m3"]));
 936    (((((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] [(`minn m2 _1`)])))) THEN (((use_arg_then2 ("minnCA", [minnCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 937 ];;
 938
 939 (* Lemma minnAC *)
 940 let minnAC = Sections.section_proof ["m1";"m2";"m3"]
 941 `minn (minn m1 m2) m3 = minn (minn m1 m3) m2`
 942 [
 943    (((((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("minnCA", [minnCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("minnA", [minnA]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 944 ];;
 945
 946 (* Lemma eqn_minr *)
 947 let eqn_minr = Sections.section_proof ["m";"n"]
 948 `(minn m n = n) = (n <= m)`
 949 [
 950    (((fun arg_tac -> (use_arg_then2 ("eqn_addr", [eqn_addr])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))));
 951    (((((use_arg_then2 ("addn_min_max", [addn_min_max]))(gsym_then (thm_tac (new_rewrite [] [(`n + m`)]))))) THEN (((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqn_addl", [eqn_addl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [(`m = _1`)])))) THEN (((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqn_maxl", [eqn_maxl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 952 ];;
 953
 954 (* Lemma eqn_minl *)
 955 let eqn_minl = Sections.section_proof ["m";"n"]
 956 `(minn m n = m) = (m <= n)`
 957 [
 958    (((((fun arg_tac -> (use_arg_then2 ("eqn_addr", [eqn_addr])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [(`_1 = m + n`)])))) THEN (((use_arg_then2 ("addn_min_max", [addn_min_max]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqn_addl", [eqn_addl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqn_maxr", [eqn_maxr]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 959 ];;
 960
 961 (* Lemma minnn *)
 962 let minnn = Sections.section_proof ["n"]
 963 `minn n n = n`
 964 [
 965    (((((use_arg_then2 ("minnr", [minnr]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 966 ];;
 967
 968 (* Lemma leq_minr *)
 969 let leq_minr = Sections.section_proof ["m";"n1";"n2"]
 970 `(m <= minn n1 n2) <=> (m <= n1) /\ (m <= n2)`
 971 [
 972    ((((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 973 ];;
 974
 975 (* Lemma leq_minl *)
 976 let leq_minl = Sections.section_proof ["m";"n1";"n2"]
 977 `(minn n1 n2 <= m) <=> (n1 <= m) \/ (n2 <= m)`
 978 [
 979    (((((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_minr", [leq_minr]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leqNgt", [leqNgt]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 980 ];;
 981
 982 (* Lemma addn_minl *)
 983 let addn_minl = Sections.section_proof []
 984 `!m1 m2 n. (minn m1 m2) + n = minn (m1 + n) (m2 + n)`
 985 [
 986    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("minn_to_maxn", [minn_to_maxn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addn_maxl", [addn_maxl]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnA", [addnA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subn_add2r", [subn_add2r]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnAC", [addnAC]))(thm_tac (new_rewrite [] []))))));
 987    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("addnC", [addnC])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 + n`)])))))) THEN (((use_arg_then2 ("addn_subA", [addn_subA]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("addn_min_max", [addn_min_max]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_addl", [leq_addl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 988 ];;
 989
 990 (* Lemma addn_minr *)
 991 let addn_minr = Sections.section_proof []
 992 `!m n1 n2. m + minn n1 n2 = minn (m + n1) (m + n2)`
 993 [
 994    (BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"]));
 995    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("addnC", [addnC])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`m + _1`)]))))) THEN (((use_arg_then2 ("addn_minl", [addn_minl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 996 ];;
 997
 998 (* Lemma maxnK *)
 999 let maxnK = Sections.section_proof ["m";"n"]
1000 `minn (maxn m n) m = m`
1001 [
1002    (((((use_arg_then2 ("minnr", [minnr]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("leq_maxr", [leq_maxr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1003 ];;
1004
1005 (* Lemma maxKn *)
1006 let maxKn = Sections.section_proof ["m";"n"]
1007 `minn n (maxn m n) = n`
1008 [
1009    (((((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("maxnK", [maxnK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1010 ];;
1011
1012 (* Lemma minnK *)
1013 let minnK = Sections.section_proof ["m";"n"]
1014 `maxn (minn m n) m = m`
1015 [
1016    (((((use_arg_then2 ("maxnr", [maxnr]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("leq_minl", [leq_minl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1017 ];;
1018
1019 (* Lemma minKn *)
1020 let minKn = Sections.section_proof ["m";"n"]
1021 `maxn n (minn m n) = n`
1022 [
1023    (((((use_arg_then2 ("minnC", [minnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("minnK", [minnK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1024 ];;
1025
1026 (* Lemma maxn_minl *)
1027 let maxn_minl = Sections.section_proof ["m1";"m2";"n"]
1028 `maxn (minn m1 m2) n = minn (maxn m1 n) (maxn m2 n)`
1029 [
1030    (((repeat_tactic 1 9 (((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] [])))))) THEN (arith_tac));
1031 ];;
1032
1033 (* Lemma maxn_minr *)
1034 let maxn_minr = Sections.section_proof ["m";"n1";"n2"]
1035 `maxn m (minn n1 n2) = minn (maxn m n1) (maxn m n2)`
1036 [
1037    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("maxnC", [maxnC])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (((use_arg_then2 ("maxn_minl", [maxn_minl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1038 ];;
1039
1040 (* Lemma minn_maxl *)
1041 let minn_maxl = Sections.section_proof []
1042 `!m1 m2 n. minn (maxn m1 m2) n = maxn (minn m1 n) (minn m2 n)`
1043 [
1044    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((((use_arg_then2 ("maxn_minr", [maxn_minr]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("maxn_minl", [maxn_minl]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("minnA", [minnA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("maxnn", [maxnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("maxnC", [maxnC]))(thm_tac (new_rewrite [] [(`maxn _1 n`)])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("maxnK", [maxnK]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1045 ];;
1046
1047 (* Lemma minn_maxr *)
1048 let minn_maxr = Sections.section_proof []
1049 `!m n1 n2. minn m (maxn n1 n2) = maxn (minn m n1) (minn m n2)`
1050 [
1051    (BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"]));
1052    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("minnC", [minnC])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`minn m _1`)]))))) THEN (((use_arg_then2 ("minn_maxl", [minn_maxl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1053 ];;
1054
1055 (* Section Iteration *)
1056 Sections.begin_section "Iteration";;
1057 (Sections.add_section_var (mk_var ("m", (`:num`))); Sections.add_section_var (mk_var ("n", (`:num`))));;
1058 (Sections.add_section_var (mk_var ("x", (`:A`))); Sections.add_section_var (mk_var ("y", (`:A`))));;
1059 let iter = define `iter (SUC n) f (x:A) = f (iter n f x) /\ iter 0 f x = x`;;
1060 let iteri = define `iteri (SUC n) f (x:A) = f n (iteri n f x) /\ iteri 0 f x = x`;;
1061
1062 (* Lemma iterSr *)
1063 let iterSr = Sections.section_proof ["n";"f";"x"]
1064 `iter (SUC n) f (x : A) = iter n f (f x)`
1065 [
1066    ((((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("iter", [iter]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (move ["n"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1067 ];;
1068
1069 (* Lemma iterS *)
1070 let iterS = Sections.section_proof ["n";"f";"x"]
1071 `iter (SUC n) f (x:A) = f (iter n f x)`
1072 [
1073    ((((use_arg_then2 ("iter", [iter]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1074 ];;
1075
1076 (* Lemma iter_add *)
1077 let iter_add = Sections.section_proof ["n";"m";"f";"x"]
1078 `iter (n + m) f (x:A) = iter n f (iter m f x)`
1079 [
1080    ((((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("iter", [iter]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (((use_arg_then2 ("add0n", [add0n]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("addSn", [addSn]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (move ["n"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("iterS", [iterS]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1081 ];;
1082
1083 (* Lemma iteriS *)
1084 let iteriS = Sections.section_proof ["n";"f";"x"]
1085 `iteri (SUC n) f x = f n (iteri n f (x:A))`
1086 [
1087    ((((use_arg_then2 ("iteri", [iteri]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1088 ];;
1089
1090 (* Finalization of the section Iteration *)
1091 let iterSr = Sections.finalize_theorem iterSr;;
1092 let iterS = Sections.finalize_theorem iterS;;
1093 let iter_add = Sections.finalize_theorem iter_add;;
1094 let iteriS = Sections.finalize_theorem iteriS;;
1095 Sections.end_section "Iteration";;
1096
1097 (* Lemma mul0n *)
1098 let mul0n = Sections.section_proof ["n"]
1099 `0 * n = 0`
1100 [
1101    ((arith_tac) THEN (done_tac));
1102 ];;
1103
1104 (* Lemma muln0 *)
1105 let muln0 = Sections.section_proof ["n"]
1106 `n * 0 = 0`
1107 [
1108    ((arith_tac) THEN (done_tac));
1109 ];;
1110
1111 (* Lemma mul1n *)
1112 let mul1n = Sections.section_proof ["n"]
1113 `1 * n = n`
1114 [
1115    ((arith_tac) THEN (done_tac));
1116 ];;
1117
1118 (* Lemma mulSn *)
1119 let mulSn = Sections.section_proof ["m";"n"]
1120 `SUC m * n = n + m * n`
1121 [
1122    (arith_tac);
1123 ];;
1124
1125 (* Lemma mulSnr *)
1126 let mulSnr = Sections.section_proof ["m";"n"]
1127 `SUC m * n = m * n + n`
1128 [
1129    (arith_tac);
1130 ];;
1131
1132 (* Lemma mulnS *)
1133 let mulnS = Sections.section_proof ["m";"n"]
1134 `m * SUC n = m + m * n`
1135 [
1136    ((((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN elim) THEN (((repeat_tactic 0 10 (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["m"])));
1137    ((((repeat_tactic 1 9 (((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnCA", [addnCA]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1138 ];;
1139
1140 (* Lemma mulnSr *)
1141 let mulnSr = Sections.section_proof ["m";"n"]
1142 `m * SUC n = m * n + m`
1143 [
1144    (((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulnS", [mulnS]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1145 ];;
1146
1147 (* Lemma muln1 *)
1148 let muln1 = Sections.section_proof ["n"]
1149 `n * 1 = n`
1150 [
1151    (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `1 = SUC 0`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulnSr", [mulnSr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("muln0", [muln0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1152 ];;
1153
1154 (* Lemma mulnC *)
1155 let mulnC = Sections.section_proof []
1156 `!m n. m * n = n * m`
1157 [
1158    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
1159    (((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; (move ["m"])]) THEN (((repeat_tactic 0 10 (((use_arg_then2 ("muln0", [muln0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mulnS", [mulnS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1160 ];;
1161
1162 (* Lemma muln_addl *)
1163 let muln_addl = Sections.section_proof ["m1";"m2";"n"]
1164 `(m1 + m2) * n = m1 * n + m2 * n`
1165 [
1166    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("m1", [])) (disch_tac [])) THEN (clear_assumption "m1") THEN elim) [ALL_TAC; ((move ["m1"]) THEN (move ["IHm"]))]) (((((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
1167    (((((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IHm", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mulSn", [mulSn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1168 ];;
1169
1170 (* Lemma muln_addr *)
1171 let muln_addr = Sections.section_proof ["m";"n1";"n2"]
1172 `m * (n1 + n2) = m * n1 + m * n2`
1173 [
1174    (((repeat_tactic 1 9 (((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (((use_arg_then2 ("muln_addl", [muln_addl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1175 ];;
1176
1177 (* Lemma muln_subl *)
1178 let muln_subl = Sections.section_proof []
1179 `!m n p. (m - n) * p = m * p - n * p`
1180 [
1181    ((THENL_FIRST) (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN ((THENL) case [ALL_TAC; (move ["n'"])])) (((repeat_tactic 1 9 (((use_arg_then2 ("muln0", [muln0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subn0", [subn0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1182    ((((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHm"]))]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN ((repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("mul0n", [mul0n]))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("sub0n", [sub0n]))(fun tmp_arg1 -> (use_arg_then2 ("subn0", [subn0]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subn_add2l", [subn_add2l]))(thm_tac (new_rewrite [] []))))));
1183    (((((use_arg_then2 ("IHm", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subSS", [subSS]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1184 ];;
1185
1186 (* Lemma muln_subr *)
1187 let muln_subr = Sections.section_proof []
1188 `!m n p. m * (n - p) = m * n - m * p`
1189 [
1190    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (((use_arg_then2 ("muln_subl", [muln_subl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1191 ];;
1192
1193 (* Lemma mulnA *)
1194 let mulnA = Sections.section_proof []
1195 `!m n p. m * (n * p) = (m * n) * p`
1196 [
1197    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
1198    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; (move ["m"])]) ((repeat_tactic 1 9 (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1199    ((((repeat_tactic 1 9 (((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("muln_addl", [muln_addl]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1200 ];;
1201
1202 (* Lemma mulnCA *)
1203 let mulnCA = Sections.section_proof ["m";"n1";"n2"]
1204 `m * (n1 * n2) = n1 * (m * n2)`
1205 [
1206    (((repeat_tactic 1 9 (((use_arg_then2 ("mulnA", [mulnA]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("mulnC", [mulnC])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (done_tac));
1207 ];;
1208
1209 (* Lemma mulnAC *)
1210 let mulnAC = Sections.section_proof ["m";"n";"p"]
1211 `(n * m) * p = (n * p) * m`
1212 [
1213    (((repeat_tactic 1 9 (((use_arg_then2 ("mulnA", [mulnA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [(`p * _1`)]))))) THEN (done_tac));
1214 ];;
1215
1216 (* Lemma muln_eq0 *)
1217 let muln_eq0 = Sections.section_proof ["m";"n"]
1218 `(m * n = 0) <=> (m = 0) \/ (n = 0)`
1219 [
1220    ((((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN ((repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("muln0", [muln0]))(fun tmp_arg1 -> (use_arg_then2 ("mul0n", [mul0n]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (arith_tac));
1221 ];;
1222
1223 (* Lemma eqn_mul1 *)
1224 let eqn_mul1 = Sections.section_proof ["m";"n"]
1225 `(m * n = 1) <=> (m = 1) /\ (n = 1)`
1226 [
1227    ((((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((THENL) case [ALL_TAC; ((THENL) case [ALL_TAC; (move ["n"])])])) THEN (arith_tac) THEN (done_tac));
1228 ];;
1229
1230 (* Lemma muln_gt0 *)
1231 let muln_gt0 = Sections.section_proof ["m";"n"]
1232 `(0 < m * n) <=> (0 < m) /\ (0 < n)`
1233 [
1234    ((((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN (arith_tac) THEN (done_tac));
1235 ];;
1236
1237 (* Lemma leq_pmull *)
1238 let leq_pmull = Sections.section_proof ["m";"n"]
1239 `0 < n ==> m <= n * m`
1240 [
1241    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("prednK", [prednK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_addr", [leq_addr]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1242 ];;
1243
1244 (* Lemma leq_pmulr *)
1245 let leq_pmulr = Sections.section_proof ["m";"n"]
1246 `0 < n ==> m <= m * n`
1247 [
1248    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("leq_pmull", [leq_pmull])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1249 ];;
1250
1251 (* Lemma leq_mul2l *)
1252 let leq_mul2l = Sections.section_proof ["m";"n1";"n2"]
1253 `(m * n1 <= m * n2) <=> (m = 0) \/ (n1 <= n2)`
1254 [
1255    (((((use_arg_then2 ("leqE", [leqE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("muln_subr", [muln_subr]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("muln_eq0", [muln_eq0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqE", [leqE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1256 ];;
1257
1258 (* Lemma leq_mul2r *)
1259 let leq_mul2r = Sections.section_proof ["m";"n1";"n2"]
1260 `(n1 * m <= n2 * m) <=> (m = 0) \/ (n1 <= n2)`
1261 [
1262    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("mulnC", [mulnC])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * m`)])))))) THEN (((use_arg_then2 ("leq_mul2l", [leq_mul2l]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1263 ];;
1264
1265 (* Lemma leq_mul *)
1266 let leq_mul = Sections.section_proof ["m1";"m2";"n1";"n2"]
1267 `m1 <= n1 ==> m2 <= n2 ==> m1 * m2 <= n1 * n2`
1268 [
1269    (BETA_TAC THEN (move ["le_mn1"]) THEN (move ["le_mn2"]));
1270    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leq_trans", [leq_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * m2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
1271    ((THENL_FIRST) (ANTS_TAC) (((((use_arg_then2 ("leq_mul2l", [leq_mul2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("le_mn2", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1272    (DISCH_THEN apply_tac);
1273    (((((use_arg_then2 ("leq_mul2r", [leq_mul2r]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("le_mn1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1274 ];;
1275
1276 (* Lemma eqn_mul2l *)
1277 let eqn_mul2l = Sections.section_proof ["m";"n1";"n2"]
1278 `(m * n1 = m * n2) <=> (m = 0) \/ (n1 = n2)`
1279 [
1280    (((((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leq_mul2l", [leq_mul2l]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("orb_andr", [orb_andr]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqn_leq", [eqn_leq]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1281 ];;
1282
1283 (* Lemma eqn_mul2r *)
1284 let eqn_mul2r = Sections.section_proof ["m";"n1";"n2"]
1285 `(n1 * m = n2 * m) <=> (m = 0) \/ (n1 = n2)`
1286 [
1287    (((((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leq_mul2r", [leq_mul2r]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("orb_andr", [orb_andr]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqn_leq", [eqn_leq]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1288 ];;
1289
1290 (* Lemma leq_pmul2l *)
1291 let leq_pmul2l = Sections.section_proof ["m";"n1";"n2"]
1292 `0 < m ==> ((m * n1 <= m * n2) <=> (n1 <= n2))`
1293 [
1294    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("prednK", [prednK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("leq_mul2l", [leq_mul2l]))(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then2 ("NOT_SUC", [NOT_SUC]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("orFb", [orFb]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1295 ];;
1296
1297 (* Lemma leq_pmul2r *)
1298 let leq_pmul2r = Sections.section_proof ["m";"n1";"n2"]
1299 `0 < m ==> ((n1 * m <= n2 * m) <=> (n1 <= n2))`
1300 [
1301    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("prednK", [prednK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("leq_mul2r", [leq_mul2r]))(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then2 ("NOT_SUC", [NOT_SUC]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("orFb", [orFb]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1302 ];;
1303
1304 (* Lemma eqn_pmul2l *)
1305 let eqn_pmul2l = Sections.section_proof ["m";"n1";"n2"]
1306 `0 < m ==> ((m * n1 = m * n2) <=> (n1 = n2))`
1307 [
1308    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("prednK", [prednK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("eqn_mul2l", [eqn_mul2l]))(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then2 ("NOT_SUC", [NOT_SUC]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("orFb", [orFb]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1309 ];;
1310
1311 (* Lemma eqn_pmul2r *)
1312 let eqn_pmul2r = Sections.section_proof ["m";"n1";"n2"]
1313 `0 < m ==> ((n1 * m = n2 * m) <=> (n1 = n2))`
1314 [
1315    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("prednK", [prednK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("eqn_mul2r", [eqn_mul2r]))(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then2 ("NOT_SUC", [NOT_SUC]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("orFb", [orFb]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1316 ];;
1317
1318 (* Lemma ltn_mul2l *)
1319 let ltn_mul2l = Sections.section_proof ["m";"n1";"n2"]
1320 `(m * n1 < m * n2) <=> (0 < m) /\ (n1 < n2)`
1321 [
1322    (((((use_arg_then2 ("lt0n", [lt0n]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_mul2l", [leq_mul2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1323 ];;
1324
1325 (* Lemma ltn_mul2r *)
1326 let ltn_mul2r = Sections.section_proof ["m";"n1";"n2"]
1327 `(n1 * m < n2 * m) <=> (0 < m) /\ (n1 < n2)`
1328 [
1329    (((((use_arg_then2 ("lt0n", [lt0n]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_mul2r", [leq_mul2r]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1330 ];;
1331
1332 (* Lemma ltn_pmul2l *)
1333 let ltn_pmul2l = Sections.section_proof ["m";"n1";"n2"]
1334 `0 < m ==> ((m * n1 < m * n2) <=> (n1 < n2))`
1335 [
1336    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("prednK", [prednK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then2 ("ltn_mul2l", [ltn_mul2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_0", [LT_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1337 ];;
1338
1339 (* Lemma ltn_pmul2r *)
1340 let ltn_pmul2r = Sections.section_proof ["m";"n1";"n2"]
1341 `0 < m ==> (n1 * m < n2 * m <=> n1 < n2)`
1342 [
1343    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("prednK", [prednK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then2 ("ltn_mul2r", [ltn_mul2r]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_0", [LT_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1344 ];;
1345
1346 (* Lemma ltn_Pmull *)
1347 let ltn_Pmull = Sections.section_proof ["m";"n"]
1348 `1 < n ==> 0 < m ==> m < n * m`
1349 [
1350    ((BETA_TAC THEN (move ["lt1n"]) THEN (move ["m_gt0"])) THEN ((((use_arg_then2 ("mul1n", [mul1n]))(gsym_then (thm_tac (new_rewrite [1] [(`m`)]))))) THEN (((use_arg_then2 ("ltn_pmul2r", [ltn_pmul2r]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1351 ];;
1352
1353 (* Lemma ltn_Pmulr *)
1354 let ltn_Pmulr = Sections.section_proof ["m";"n"]
1355 `1 < n ==> 0 < m ==> m < m * n`
1356 [
1357    ((BETA_TAC THEN (move ["lt1n"]) THEN (move ["m_gt0"])) THEN ((((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltn_Pmull", [ltn_Pmull]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1358 ];;
1359
1360 (* Lemma ltn_mul *)
1361 let ltn_mul = Sections.section_proof ["m1";"m2";"n1";"n2"]
1362 `m1 < n1 ==> m2 < n2 ==> m1 * m2 < n1 * n2`
1363 [
1364    (BETA_TAC THEN (move ["lt_mn1"]) THEN (move ["lt_mn2"]));
1365    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leq_ltn_trans", [leq_ltn_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m1 * m2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
1366    (ANTS_TAC);
1367    (((((use_arg_then2 ("leq_mul2l", [leq_mul2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbC", [orbC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnW", [ltnW]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1368    (DISCH_THEN apply_tac);
1369    ((((use_arg_then2 ("ltn_pmul2r", [ltn_pmul2r]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
1370    ((((use_arg_then2 ("lt_mn2", [])) (disch_tac [])) THEN (clear_assumption "lt_mn2") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
1371 ];;
1372
1373 (* Lemma maxn_mulr *)
1374 let maxn_mulr = Sections.section_proof ["m";"n1";"n2"]
1375 `m * maxn n1 n2 = maxn (m * n1) (m * n2)`
1376 [
1377    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["n"])]) (((repeat_tactic 1 9 (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("maxnn", [maxnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1378    (((repeat_tactic 1 9 (((use_arg_then2 ("maxn", [maxn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fun_if", [fun_if]))(thm_tac (new_rewrite [] [(`SUC n * _1`)])))) THEN (((use_arg_then2 ("ltn_pmul2l", [ltn_pmul2l]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("LT_0", [LT_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1379 ];;
1380
1381 (* Lemma maxn_mull *)
1382 let maxn_mull = Sections.section_proof ["m1";"m2";"n"]
1383 `maxn m1 m2 * n = maxn (m1 * n) (m2 * n)`
1384 [
1385    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("mulnC", [mulnC])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * n`)])))))) THEN (((use_arg_then2 ("maxn_mulr", [maxn_mulr]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1386 ];;
1387
1388 (* Lemma minn_mulr *)
1389 let minn_mulr = Sections.section_proof ["m";"n1";"n2"]
1390 `m * minn n1 n2 = minn (m * n1) (m * n2)`
1391 [
1392    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["n"])]) (((repeat_tactic 1 9 (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("if_same", [if_same]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1393    ((repeat_tactic 1 9 (((use_arg_then2 ("minn", [minn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fun_if", [fun_if]))(thm_tac (new_rewrite [] [(`SUC n * _1`)])))) THEN (((use_arg_then2 ("ltn_pmul2l", [ltn_pmul2l]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("LT_0", [LT_0]))(thm_tac (new_rewrite [] [])))));
1394 ];;
1395
1396 (* Lemma minn_mull *)
1397 let minn_mull = Sections.section_proof ["m1";"m2";"n"]
1398 `minn m1 m2 * n = minn (m1 * n) (m2 * n)`
1399 [
1400    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("mulnC", [mulnC])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * n`)])))))) THEN (((use_arg_then2 ("minn_mulr", [minn_mulr]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1401 ];;
1402 parse_as_infix("^", (24, "left"));;
1403 override_interface("^", `EXP`);;
1404
1405 (* Lemma expn0 *)
1406 let expn0 = Sections.section_proof ["m"]
1407 `m ^ 0 = 1`
1408 [
1409    ((((use_arg_then2 ("EXP", [EXP]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1410 ];;
1411
1412 (* Lemma expn1 *)
1413 let expn1 = Sections.section_proof ["m"]
1414 `m ^ 1 = m`
1415 [
1416    ((((use_arg_then2 ("EXP_1", [EXP_1]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1417 ];;
1418
1419 (* Lemma expnS *)
1420 let expnS = Sections.section_proof ["m";"n"]
1421 `m ^ SUC n = m * m ^ n`
1422 [
1423    ((((use_arg_then2 ("EXP", [EXP]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1424 ];;
1425
1426 (* Lemma expnSr *)
1427 let expnSr = Sections.section_proof ["m";"n"]
1428 `m ^ SUC n = m ^ n * m`
1429 [
1430    (((((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1431 ];;
1432
1433 (* Lemma exp0n *)
1434 let exp0n = Sections.section_proof ["n"]
1435 `0 < n ==> 0 ^ n = 0`
1436 [
1437    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) ((((use_arg_then2 ("LT_REFL", [LT_REFL]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
1438    (((((use_arg_then2 ("EXP", [EXP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1439 ];;
1440
1441 (* Lemma exp1n *)
1442 let exp1n = Sections.section_proof ["n"]
1443 `1 ^ n = 1`
1444 [
1445    (((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [(((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))); ((((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mul1n", [mul1n]))(thm_tac (new_rewrite [] [])))))]) THEN (done_tac));
1446 ];;
1447
1448 (* Lemma expn_add *)
1449 let expn_add = Sections.section_proof ["m";"n1";"n2"]
1450 `m ^ (n1 + n2) = m ^ n1 * m ^ n2`
1451 [
1452    (((THENL) (((use_arg_then2 ("n1", [])) (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mul1n", [mul1n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] [])))))));
1453    (((((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulnA", [mulnA]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1454 ];;
1455
1456 (* Lemma expn_mull *)
1457 let expn_mull = Sections.section_proof ["m1";"m2";"n"]
1458 `(m1 * m2) ^ n = m1 ^ n * m2 ^ n`
1459 [
1460    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((repeat_tactic 1 9 (((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("muln1", [muln1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1461    (((repeat_tactic 1 9 (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mulnA", [mulnA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("mulnCA", [mulnCA]))(thm_tac (new_rewrite [] [(`m2 * _1`)]))))) THEN (done_tac));
1462 ];;
1463
1464 (* Lemma expn_mulr *)
1465 let expn_mulr = Sections.section_proof ["m";"n1";"n2"]
1466 `m ^ (n1 * n2) = (m ^ n1) ^ n2`
1467 [
1468    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n1", [])) (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) (((repeat_tactic 1 9 (((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("exp1n", [exp1n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1469    (((((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("expn_add", [expn_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("expn_mull", [expn_mull]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1470 ];;
1471
1472 (* Lemma expn_gt0 *)
1473 let expn_gt0 = Sections.section_proof ["m";"n"]
1474 `(0 < m ^ n) <=> (0 < m) \/ (n = 0)`
1475 [
1476    ((THENL_FIRST) (((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))])) ((((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
1477    (((((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
1478    ((((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
1479    (((((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn_gt0", [addn_gt0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
1480 ];;
1481
1482 (* Lemma expn_eq0 *)
1483 let expn_eq0 = Sections.section_proof ["m";"e"]
1484 `(m ^ e = 0) <=> (m = 0) /\ (0 < e)`
1485 [
1486    (((repeat_tactic 1 9 (((use_arg_then2 ("eqn0Ngt", [eqn0Ngt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("expn_gt0", [expn_gt0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lt0n", [lt0n]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1487 ];;
1488
1489 (* Lemma ltn_expl *)
1490 let ltn_expl = Sections.section_proof ["m";"n"]
1491 `1 < m ==> n < m ^ n`
1492 [
1493    ((THENL_FIRST) ((BETA_TAC THEN (move ["m_gt1"])) THEN ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])])) ((((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
1494    ((((fun arg_tac -> (use_arg_then2 ("ltnW", [ltnW])) (fun fst_arg -> (use_arg_then2 ("m_gt1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("leq_pmul2l", [leq_pmul2l])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC));
1495    (((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
1496    ((((use_arg_then2 ("leq_trans", [leq_trans])) (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] []))))));
1497    ((((fun arg_tac -> (use_arg_then2 ("ltn_Pmull", [ltn_Pmull])) (fun fst_arg -> (use_arg_then2 ("m_gt1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (arith_tac) THEN (done_tac));
1498 ];;
1499
1500 (* Lemma leq_exp2l *)
1501 let leq_exp2l = Sections.section_proof ["m";"n1";"n2"]
1502 `1 < m ==> (m ^ n1 <= m ^ n2 <=> n1 <= n2)`
1503 [
1504    ((THENL_ROT (-1)) ((BETA_TAC THEN (move ["m_gt1"])) THEN ((THENL) (((use_arg_then2 ("n2", [])) (disch_tac [])) THEN (clear_assumption "n2") THEN ((use_arg_then2 ("n1", [])) (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) THEN (BETA_TAC THEN ((THENL) case [ALL_TAC; (move ["q"])])) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))));
1505    (((repeat_tactic 1 9 (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_pmul2l", [leq_pmul2l]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("leqSS", [leqSS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnW", [ltnW]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1506    (((((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("expn_gt0", [expn_gt0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("m_gt1", [])) (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
1507    ((((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))));
1508    ((((use_arg_then2 ("m_gt1", [])) (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN ((((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))) THEN (move ["m_gt1"])));
1509    ((((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("leq_trans", [leq_trans])) (fun fst_arg -> (use_arg_then2 ("m_gt1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ltE", [ltE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ltn0", [ltn0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_pmulr", [leq_pmulr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("expn_gt0", [expn_gt0]))(thm_tac (new_rewrite [] [])))));
1510    ((((use_arg_then2 ("m_gt1", [])) (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
1511 ];;
1512
1513 (* Lemma ltn_exp2l *)
1514 let ltn_exp2l = Sections.section_proof ["m";"n1";"n2"]
1515 `1 < m ==> (m ^ n1 < m ^ n2 <=> n1 < n2)`
1516 [
1517    ((BETA_TAC THEN (move ["m_gt1"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_exp2l", [leq_exp2l]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1518 ];;
1519
1520 (* Lemma eqn_exp2l *)
1521 let eqn_exp2l = Sections.section_proof ["m";"n1";"n2"]
1522 `1 < m ==> (m ^ n1 = m ^ n2 <=> n1 = n2)`
1523 [
1524    ((BETA_TAC THEN (move ["m_gt1"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leq_exp2l", [leq_exp2l]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1525 ];;
1526
1527 (* Lemma expnI *)
1528 let expnI = Sections.section_proof ["m"]
1529 `1 < m ==> !e1 e2. m ^ e1 = m ^ e2 ==> e1 = e2`
1530 [
1531    ((BETA_TAC THEN (move ["m_gt1"]) THEN (move ["e1"]) THEN (move ["e2"])) THEN (((use_arg_then2 ("eqn_exp2l", [eqn_exp2l]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1532 ];;
1533
1534 (* Lemma leq_pexp2l *)
1535 let leq_pexp2l = Sections.section_proof ["m";"n1";"n2"]
1536 `0 < m ==> n1 <= n2 ==> m ^ n1 <= m ^ n2`
1537 [
1538    (((THENL) (((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("ltn0", [ltn0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))) [((((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("exp1n", [exp1n]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("leq_exp2l", [leq_exp2l]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))]) THEN (arith_tac) THEN (done_tac));
1539 ];;
1540
1541 (* Lemma ltn_pexp2l *)
1542 let ltn_pexp2l = Sections.section_proof ["m";"n1";"n2"]
1543 `0 < m ==> m ^ n1 < m ^ n2 ==> n1 < n2`
1544 [
1545    (((THENL) (((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("ltn0", [ltn0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))) [((((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("exp1n", [exp1n]))(thm_tac (new_rewrite [] [])))))); (((use_arg_then2 ("ltn_exp2l", [ltn_exp2l]))(thm_tac (new_rewrite [] []))))]) THEN (arith_tac) THEN (done_tac));
1546 ];;
1547
1548 (* Lemma ltn_exp2r *)
1549 let ltn_exp2r = Sections.section_proof ["m";"n";"e"]
1550 `0 < e ==> (m ^ e < n ^ e <=> m < n)`
1551 [
1552    ((BETA_TAC THEN (move ["e_gt0"])) THEN ((THENL) (split_tac) [ALL_TAC; (move ["ltmn"])]));
1553    ((repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (move ["lemn"])));
1554    (((THENL) (((use_arg_then2 ("e", [])) (disch_tac [])) THEN (clear_assumption "e") THEN elim) [ALL_TAC; ((move ["e'"]) THEN (move ["IHe"]))]) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_mul", [leq_mul]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1555    ((THENL_FIRST) (((use_arg_then2 ("e_gt0", [])) (disch_tac [])) THEN (clear_assumption "e_gt0") THEN ((use_arg_then2 ("e", [])) (disch_tac [])) THEN (clear_assumption "e") THEN elim) ((((use_arg_then2 ("ltnn", [ltnn]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
1556    ((THENL_FIRST) (BETA_TAC THEN ((THENL) case [ALL_TAC; ((move ["e"]) THEN (move ["IHe"]))])) (((((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("expn1", [expn1]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
1557    (((repeat_tactic 1 9 (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ltn_mul", [ltn_mul]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("expnS", [expnS]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("IHe", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac));
1558 ];;
1559
1560 (* Lemma leq_exp2r *)
1561 let leq_exp2r = Sections.section_proof ["m";"n";"e"]
1562 `0 < e ==> (m ^ e <= n ^ e <=> m <= n)`
1563 [
1564    ((BETA_TAC THEN (move ["e_gt0"])) THEN ((((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltn_exp2r", [ltn_exp2r]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1565 ];;
1566
1567 (* Lemma eqn_exp2r *)
1568 let eqn_exp2r = Sections.section_proof ["m";"n";"e"]
1569 `0 < e ==> (m ^ e = n ^ e <=> m = n)`
1570 [
1571    ((BETA_TAC THEN (move ["e_gt0"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leq_exp2r", [leq_exp2r]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1572 ];;
1573
1574 (* Lemma expIn *)
1575 let expIn = Sections.section_proof ["e"]
1576 `0 < e ==> !m n. m ^ e = n ^ e ==> m = n`
1577 [
1578    ((BETA_TAC THEN (move ["e_gt0"]) THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then2 ("eqn_exp2r", [eqn_exp2r]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1579 ];;
1580
1581 (* Lemma fact0 *)
1582 let fact0 = Sections.section_proof []
1583 `FACT 0 = 1`
1584 [
1585    ((((use_arg_then2 ("FACT", [FACT]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1586 ];;
1587
1588 (* Lemma factS *)
1589 let factS = Sections.section_proof ["n"]
1590 `FACT (SUC n)  = (SUC n) * FACT n`
1591 [
1592    ((((use_arg_then2 ("FACT", [FACT]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1593 ];;
1594
1595 (* Lemma fact_gt0 *)
1596 let fact_gt0 = Sections.section_proof ["n"]
1597 `0 < FACT n`
1598 [
1599    (((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])]) THEN ((((use_arg_then2 ("FACT", [FACT]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("muln_gt0", [muln_gt0]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))))) THEN (arith_tac) THEN (done_tac));
1600 ];;
1601 let odd = new_basic_definition `odd = ODD`;;
1602
1603 (* Lemma odd0 *)
1604 let odd0 = Sections.section_proof []
1605 `odd 0 = F`
1606 [
1607    ((((use_arg_then2 ("odd", [odd]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 2 0 (((use_arg_then2 ("ODD", [ODD]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1608 ];;
1609
1610 (* Lemma oddS *)
1611 let oddS = Sections.section_proof ["n"]
1612 `odd (SUC n) = ~odd n`
1613 [
1614    (((((use_arg_then2 ("odd", [odd]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("ODD", [ODD]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1615 ];;
1616
1617 (* Lemma odd1 *)
1618 let odd1 = Sections.section_proof []
1619 `odd 1 = T`
1620 [
1621    (((((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("oddS", [oddS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd0", [odd0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1622 ];;
1623
1624 (* Lemma odd_add *)
1625 let odd_add = Sections.section_proof ["m";"n"]
1626 `odd (m + n) = odd m + odd n`
1627 [
1628    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHn"]))]) (((((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd0", [odd0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addFb", [addFb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1629    (((((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("oddS", [oddS]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addTb", [addTb]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addbA", [addbA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addTb", [addTb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1630 ];;
1631
1632 (* Lemma odd_sub *)
1633 let odd_sub = Sections.section_proof ["m";"n"]
1634 `n <= m ==> odd (m - n) = odd m + odd n`
1635 [
1636    ((BETA_TAC THEN (move ["le_nm"])) THEN (((fun arg_tac -> (use_arg_then2 ("addIb", [addIb])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`odd n`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("odd_add", [odd_add]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("addbK", [addbK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1637 ];;
1638
1639 (* Lemma odd_opp *)
1640 let odd_opp = Sections.section_proof ["i";"m"]
1641 `odd m = F ==> i < m ==> odd (m - i) = odd i`
1642 [
1643    (BETA_TAC THEN (move ["oddm"]) THEN (move ["lt_im"]));
1644    (((((fun arg_tac -> (use_arg_then2 ("odd_sub", [odd_sub])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("ltnW", [ltnW])) (fun fst_arg -> (use_arg_then2 ("lt_im", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("oddm", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addFb", [addFb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1645 ];;
1646
1647 (* Lemma odd_mul *)
1648 let odd_mul = Sections.section_proof ["m";"n"]
1649 `odd (m * n) <=> odd m /\ odd n`
1650 [
1651    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHm"]))]) (((((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd0", [odd0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andFb", [andFb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1652    (((((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd_add", [odd_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("oddS", [oddS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addTb", [addTb]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andb_addl", [andb_addl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IHm", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1653 ];;
1654
1655 (* Lemma odd_exp *)
1656 let odd_exp = Sections.section_proof ["m";"n"]
1657 `odd (m ^ n) <=> (n = 0) \/ odd m`
1658 [
1659    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd1", [odd1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1660    ((((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd_mul", [odd_mul]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbC", [orbC]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `SUC n = 0 <=> F`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))));
1661    ((fun arg_tac -> arg_tac (Arg_term (`odd m`))) (term_tac (set_tac "b")));
1662    (((use_arg_then2 ("IHn", [])) (disch_tac [])) THEN (clear_assumption "IHn") THEN ((use_arg_then2 ("b_def", [])) (disch_tac [])) THEN (clear_assumption "b_def") THEN BETA_TAC THEN (move ["_"]) THEN (move ["_"]));
1663    ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
1664 ];;
1665 let double = define `double 0 = 0 /\ (!n. double (SUC n) = SUC (SUC (double n)))`;;
1666
1667 (* Lemma double0 *)
1668 let double0 = Sections.section_proof []
1669 `double 0 = 0`
1670 [
1671    ((((use_arg_then2 ("double", [double]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1672 ];;
1673
1674 (* Lemma doubleS *)
1675 let doubleS = Sections.section_proof ["n"]
1676 `double (SUC n) = SUC (SUC (double n))`
1677 [
1678    ((((use_arg_then2 ("double", [double]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1679 ];;
1680
1681 (* Lemma addnn *)
1682 let addnn = Sections.section_proof ["n"]
1683 `n + n = double n`
1684 [
1685    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1686    (((((use_arg_then2 ("addnS", [addnS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("doubleS", [doubleS]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1687 ];;
1688
1689 (* Lemma mul2n *)
1690 let mul2n = Sections.section_proof ["m"]
1691 `2 * m = double m`
1692 [
1693    (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `2 = SUC 1`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulSn", [mulSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mul1n", [mul1n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnn", [addnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1694 ];;
1695
1696 (* Lemma muln2 *)
1697 let muln2 = Sections.section_proof ["m"]
1698 `m * 2 = double m`
1699 [
1700    (((((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mul2n", [mul2n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1701 ];;
1702
1703 (* Lemma double_add *)
1704 let double_add = Sections.section_proof ["m";"n"]
1705 `double (m + n) = double m + double n`
1706 [
1707    (((repeat_tactic 1 9 (((use_arg_then2 ("addnn", [addnn]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then2 ("addnCA", [addnCA])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`n + _1`)]))))) THEN (done_tac));
1708 ];;
1709
1710 (* Lemma double_sub *)
1711 let double_sub = Sections.section_proof ["m";"n"]
1712 `double (m - n) = double m - double n`
1713 [
1714    ((((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then2 ("m", [])) (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHm"]))]) THEN ((THENL) case [ALL_TAC; (move ["n"])])) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("sub0n", [sub0n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("subn0", [subn0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("subn0", [subn0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("sub0n", [sub0n]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
1715    (((repeat_tactic 1 9 (((use_arg_then2 ("doubleS", [doubleS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("subSS", [subSS]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IHm", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1716 ];;
1717
1718 (* Lemma leq_double *)
1719 let leq_double = Sections.section_proof ["m";"n"]
1720 `(double m <= double n <=> m <= n)`
1721 [
1722    (((repeat_tactic 1 9 (((use_arg_then2 ("leqE", [leqE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("double_sub", [double_sub]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((THENL) (((fun arg_tac -> arg_tac (Arg_term (`m - n`))) (disch_tac [])) THEN case) [ALL_TAC; (move ["n"])]) THEN (((use_arg_then2 ("double", [double]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
1723 ];;
1724
1725 (* Lemma ltn_double *)
1726 let ltn_double = Sections.section_proof ["m";"n"]
1727 `(double m < double n) = (m < n)`
1728 [
1729    (((repeat_tactic 2 0 (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_double", [leq_double]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1730 ];;
1731
1732 (* Lemma ltn_Sdouble *)
1733 let ltn_Sdouble = Sections.section_proof ["m";"n"]
1734 `(SUC (double m) < double n) = (m < n)`
1735 [
1736    ((repeat_tactic 1 9 (((use_arg_then2 ("muln2", [muln2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
1737 ];;
1738
1739 (* Lemma leq_Sdouble *)
1740 let leq_Sdouble = Sections.section_proof ["m";"n"]
1741 `(double m <= SUC (double n)) = (m <= n)`
1742 [
1743    (((((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltn_Sdouble", [ltn_Sdouble]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1744 ];;
1745
1746 (* Lemma odd_double *)
1747 let odd_double = Sections.section_proof ["n"]
1748 `odd (double n) = F`
1749 [
1750    (((((use_arg_then2 ("addnn", [addnn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("odd_add", [odd_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addbb", [addbb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1751 ];;
1752
1753 (* Lemma double_gt0 *)
1754 let double_gt0 = Sections.section_proof ["n"]
1755 `(0 < double n) = (0 < n)`
1756 [
1757    (((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("doubleS", [doubleS]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac));
1758 ];;
1759
1760 (* Lemma double_eq0 *)
1761 let double_eq0 = Sections.section_proof ["n"]
1762 `(double n = 0) = (n = 0)`
1763 [
1764    (((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("doubleS", [doubleS]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac));
1765 ];;
1766
1767 (* Lemma double_mull *)
1768 let double_mull = Sections.section_proof ["m";"n"]
1769 `double (m * n) = double m * n`
1770 [
1771    (((repeat_tactic 1 9 (((use_arg_then2 ("mul2n", [mul2n]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("mulnA", [mulnA]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1772 ];;
1773
1774 (* Lemma double_mulr *)
1775 let double_mulr = Sections.section_proof ["m";"n"]
1776 `double (m * n) = m * double n`
1777 [
1778    (((repeat_tactic 1 9 (((use_arg_then2 ("muln2", [muln2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("mulnA", [mulnA]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1779 ];;
1780 let half_def = define `HALF 0 = (0, 0) /\
1781         !n. HALF (SUC n) = (SND (HALF n), SUC (FST (HALF n)))`;;
1782 let half = new_basic_definition `half = FST o HALF`;;
1783 let uphalf = new_basic_definition `uphalf = SND o HALF`;;
1784
1785 (* Lemma half0 *)
1786 let half0 = Sections.section_proof []
1787 `half 0 = 0`
1788 [
1789    (((((use_arg_then2 ("half", [half]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("o_DEF", [o_DEF]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then2 ("half_def", [half_def]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1790 ];;
1791
1792 (* Lemma uphalf0 *)
1793 let uphalf0 = Sections.section_proof []
1794 `uphalf 0 = 0`
1795 [
1796    (((((use_arg_then2 ("uphalf", [uphalf]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("o_DEF", [o_DEF]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then2 ("half_def", [half_def]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1797 ];;
1798
1799 (* Lemma halfS *)
1800 let halfS = Sections.section_proof ["n"]
1801 `half (SUC n) = uphalf n`
1802 [
1803    (((((use_arg_then2 ("half", [half]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("uphalf", [uphalf]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("o_DEF", [o_DEF]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then2 ("half_def", [half_def]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1804 ];;
1805
1806 (* Lemma uphalfS *)
1807 let uphalfS = Sections.section_proof ["n"]
1808 `uphalf (SUC n) = SUC (half n)`
1809 [
1810    (((((use_arg_then2 ("half", [half]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("uphalf", [uphalf]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("o_DEF", [o_DEF]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then2 ("half_def", [half_def]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1811 ];;
1812
1813 (* Lemma doubleK *)
1814 let doubleK = Sections.section_proof ["x"]
1815 `half (double x) = x`
1816 [
1817    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN elim) [ALL_TAC; (move ["n"])]) (((((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("half0", [half0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1818    ((((((use_arg_then2 ("doubleS", [doubleS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("halfS", [halfS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uphalfS", [uphalfS]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1819 ];;
1820 let half_double = doubleK;;
1821
1822 (* Lemma double_inj *)
1823 let double_inj = Sections.section_proof []
1824 `!m n. double m = double n ==> m = n`
1825 [
1826    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
1827    ((((((use_arg_then2 ("doubleK", [doubleK]))(gsym_then (thm_tac (new_rewrite [2] [(`m`)]))))) THEN (((use_arg_then2 ("doubleK", [doubleK]))(gsym_then (thm_tac (new_rewrite [2] [(`n`)])))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1828 ];;
1829
1830 (* Lemma uphalf_double *)
1831 let uphalf_double = Sections.section_proof ["n"]
1832 `uphalf (double n) = n`
1833 [
1834    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])]) (((((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uphalf0", [uphalf0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1835    ((((((use_arg_then2 ("doubleS", [doubleS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uphalfS", [uphalfS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("halfS", [halfS]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1836 ];;
1837
1838 (* Lemma uphalf_half *)
1839 let uphalf_half = Sections.section_proof ["n"]
1840 `uphalf n = (if odd n then 1 else 0) + half n`
1841 [
1842    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then2 ("uphalf0", [uphalf0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("half0", [half0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd0", [odd0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1843    ((((use_arg_then2 ("halfS", [halfS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IHn", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnA", [addnA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("oddS", [oddS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uphalfS", [uphalfS]))(thm_tac (new_rewrite [] [])))));
1844    ((((fun arg_tac -> arg_tac (Arg_term (`odd n`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((fun arg_tac ->(use_arg_then2 ("add0n", [add0n]))(fun tmp_arg1 -> (use_arg_then2 ("addn0", [addn0]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1845 ];;
1846
1847 (* Lemma odd_double_half *)
1848 let odd_double_half = Sections.section_proof ["n"]
1849 `(if odd n then 1 else 0) + double (half n) = n`
1850 [
1851    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then2 ("odd0", [odd0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("half0", [half0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1852    ((((use_arg_then2 ("IHn", []))(gsym_then (thm_tac (new_rewrite [3] []))))) THEN (((use_arg_then2 ("halfS", [halfS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uphalf_half", [uphalf_half]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("double_add", [double_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("oddS", [oddS]))(thm_tac (new_rewrite [] [])))));
1853    (((use_arg_then2 ("IHn", [])) (disch_tac [])) THEN (clear_assumption "IHn") THEN BETA_TAC THEN (move ["_"]));
1854    ((((fun arg_tac -> arg_tac (Arg_term (`odd n`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("doubleS", [doubleS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("double0", [double0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1855 ];;
1856
1857 (* Lemma half_bit_double *)
1858 let half_bit_double = Sections.section_proof ["n";"b"]
1859 `half ((if b then 1 else 0) + double n) = n`
1860 [
1861    ((((use_arg_then2 ("b", [])) (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN ((simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("halfS", [halfS]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac ->(use_arg_then2 ("half_double", [half_double]))(fun tmp_arg1 -> (use_arg_then2 ("uphalf_double", [uphalf_double]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1862 ];;
1863
1864 (* Lemma half_add *)
1865 let half_add = Sections.section_proof ["m";"n"]
1866 `half (m + n) = (if odd m /\ odd n then 1 else 0) + (half m + half n)`
1867 [
1868    ((((use_arg_then2 ("odd_double_half", [odd_double_half]))(gsym_then (thm_tac (new_rewrite [1] [(`n`)]))))) THEN (((use_arg_then2 ("addnCA", [addnCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("odd_double_half", [odd_double_half]))(gsym_then (thm_tac (new_rewrite [1] [(`m`)]))))) THEN (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("double_add", [double_add]))(gsym_then (thm_tac (new_rewrite [] []))))));
1869    ((repeat_tactic 2 0 ((((fun arg_tac -> arg_tac (Arg_term (`odd _`))) (disch_tac [])) THEN case))) THEN ((simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("half_double", [half_double]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("halfS", [halfS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uphalfS", [uphalfS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uphalf_double", [uphalf_double]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
1870    ((((use_arg_then2 ("half_double", [half_double]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1871 ];;
1872
1873 (* Lemma half_leq *)
1874 let half_leq = Sections.section_proof ["m";"n"]
1875 `m <= n ==> half m <= half n`
1876 [
1877    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("subnK", [subnK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((((use_arg_then2 ("half_add", [half_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnA", [addnA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq_addl", [leq_addl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1878 ];;
1879
1880 (* Lemma half_gt0 *)
1881 let half_gt0 = Sections.section_proof ["n"]
1882 `(0 < half n) = (1 < n)`
1883 [
1884    (((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (case THEN ALL_TAC)]) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("halfS", [halfS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uphalfS", [uphalfS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uphalf0", [uphalf0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("half0", [half0]))(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
1885 ];;
1886
1887 (* Lemma mulnn *)
1888 let mulnn = Sections.section_proof ["m"]
1889 `m * m = m ^ 2`
1890 [
1891    (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `2 = SUC (SUC 0)`)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("expnS", [expnS]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("expn0", [expn0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("muln1", [muln1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1892 ];;
1893
1894 (* Lemma sqrn_add *)
1895 let sqrn_add = Sections.section_proof ["m";"n"]
1896 `(m + n) ^ 2 = (m ^ 2 + n ^ 2) + 2 * (m * n)`
1897 [
1898    ((repeat_tactic 1 9 (((use_arg_then2 ("mulnn", [mulnn]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("mul2n", [mul2n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("muln_addr", [muln_addr]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("muln_addl", [muln_addl]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("mulnC", [mulnC])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] [])))))));
1899    (((((use_arg_then2 ("EQ_ADD_LCANCEL", [EQ_ADD_LCANCEL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnA", [addnA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnn", [addnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1900 ];;
1901
1902 (* Lemma sqrn_sub *)
1903 let sqrn_sub = Sections.section_proof ["m";"n"]
1904 `n <= m ==> (m - n) ^ 2 = (m ^ 2 + n ^ 2) - 2 * (m * n)`
1905 [
1906    ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("subnK", [subnK])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["def_m"]));
1907    ((((use_arg_then2 ("def_m", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("sqrn_add", [sqrn_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnAC", [addnAC]))(thm_tac (new_rewrite [] [])))));
1908    (((repeat_tactic 2 0 (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("addnn", [addnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mul2n", [mul2n]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("muln_addr", [muln_addr]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mulnn", [mulnn]))(gsym_then (thm_tac (new_rewrite [] [(`n EXP 2`)]))))) THEN (((use_arg_then2 ("muln_addl", [muln_addl]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("def_m", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnK", [addnK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1909 ];;
1910
1911 (* Lemma sqrn_add_sub *)
1912 let sqrn_add_sub = Sections.section_proof ["m";"n"]
1913 `n <= m ==> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2`
1914 [
1915    ((BETA_TAC THEN (move ["le_nm"])) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `4 = 2 * 2`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulnA", [mulnA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mul2n", [mul2n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnn", [addnn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subn_sub", [subn_sub]))(gsym_then (thm_tac (new_rewrite [] [])))))));
1916    (((((use_arg_then2 ("sqrn_add", [sqrn_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnK", [addnK]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("sqrn_sub", [sqrn_sub]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1917 ];;
1918
1919 (* Lemma subn_sqr *)
1920 let subn_sqr = Sections.section_proof ["m";"n"]
1921 `m ^ 2 - n ^ 2 = (m - n) * (m + n)`
1922 [
1923    (((((use_arg_then2 ("muln_subl", [muln_subl]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("muln_addr", [muln_addr]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("mulnC", [mulnC])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subn_add2l", [subn_add2l]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mulnn", [mulnn]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1924 ];;
1925
1926 (* Lemma ltn_sqr *)
1927 let ltn_sqr = Sections.section_proof ["m";"n"]
1928 `(m ^ 2 < n ^ 2) = (m < n)`
1929 [
1930    (((((use_arg_then2 ("ltn_exp2r", [ltn_exp2r]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
1931 ];;
1932
1933 (* Lemma leq_sqr *)
1934 let leq_sqr = Sections.section_proof ["m";"n"]
1935 `(m ^ 2 <= n ^ 2) = (m <= n)`
1936 [
1937    (((((use_arg_then2 ("leq_exp2r", [leq_exp2r]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
1938 ];;
1939
1940 (* Lemma sqrn_gt0 *)
1941 let sqrn_gt0 = Sections.section_proof ["n"]
1942 `(0 < n ^ 2) = (0 < n)`
1943 [
1944    ((THENL_FIRST) ((((fun arg_tac -> (use_arg_then2 ("ltn_sqr", [ltn_sqr])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("exp0n", [exp0n]))(thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac)));
1945    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1946 ];;
1947
1948 (* Lemma eqn_sqr *)
1949 let eqn_sqr = Sections.section_proof ["m";"n"]
1950 `(m ^ 2 = n ^ 2) = (m = n)`
1951 [
1952    (((((use_arg_then2 ("eqn_exp2r", [eqn_exp2r]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
1953 ];;
1954
1955 (* Lemma sqrn_inj *)
1956 let sqrn_inj = Sections.section_proof ["m";"n"]
1957 `m ^ 2 = n ^ 2 ==> m = n`
1958 [
1959    (BETA_TAC THEN (move ["eq"]));
1960    (((fun arg_tac -> (use_arg_then2 ("expIn", [expIn])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `0 < 2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["inj"]));
1961    ((((fun arg_tac -> (use_arg_then2 ("inj", [])) (fun fst_arg -> (use_arg_then2 ("eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1962 ];;
1963 let leqif = new_definition `!m n c. leqif m n c <=> (m <= n /\ ((m = n) <=> c))`;;
1964
1965 (* Lemma leqifP *)
1966 let leqifP = Sections.section_proof ["m";"n";"c"]
1967 `leqif m n c <=> if c then m = n else m < n`
1968 [
1969    ((THENL_FIRST) (((((use_arg_then2 ("ltn_neqAle", [ltn_neqAle]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] []))))) THEN (split_tac)) ((((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac)));
1970    ((((use_arg_then2 ("c", [])) (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1971 ];;
1972
1973 (* Lemma leqif_imp_le *)
1974 let leqif_imp_le = Sections.section_proof ["m";"n";"c"]
1975 `leqif m n c ==> m <= n`
1976 [
1977    (((((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
1978 ];;
1979
1980 (* Lemma leqif_imp_eq *)
1981 let leqif_imp_eq = Sections.section_proof ["m";"n";"c"]
1982 `leqif m n c ==> (m = n <=> c)`
1983 [
1984    (((((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
1985 ];;
1986
1987 (* Lemma leqif_refl *)
1988 let leqif_refl = Sections.section_proof ["m";"c"]
1989 `(leqif m m c) <=> c`
1990 [
1991    (((((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1992 ];;
1993
1994 (* Lemma leqif_trans *)
1995 let leqif_trans = Sections.section_proof ["m1";"m2";"m3";"c1";"c2"]
1996 `leqif m1 m2 c1 ==> leqif m2 m3 c2 ==> leqif m1 m3 (c1 /\ c2)`
1997 [
1998    (repeat_tactic 1 9 (((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] [])))));
1999    ((THENL_FIRST) ((((use_arg_then2 ("c1", [])) (disch_tac [])) THEN (clear_assumption "c1") THEN case) THEN (((use_arg_then2 ("c2", [])) (disch_tac [])) THEN (clear_assumption "c2") THEN case THEN (simp_tac) THEN (move ["lt12"]))) ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
2000    ((repeat_tactic 1 9 (((use_arg_then2 ("ltE", [ltE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq_trans", [leq_trans])) (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("leqSS", [leqSS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnW", [ltnW])) (disch_tac [])) THEN (clear_assumption "ltnW") THEN (exact_tac)) THEN (done_tac));
2001 ];;
2002
2003 (* Lemma monotone_leqif *)
2004 let monotone_leqif = Sections.section_proof ["f"]
2005 `(!m n. f m <= f n <=> m <= n) ==>
2006   !m n c. (leqif (f m) (f n) c) <=> (leqif m n c)`
2007 [
2008    (BETA_TAC THEN (move ["f_mono"]) THEN (move ["m"]) THEN (move ["n"]) THEN (move ["c"]));
2009    (((repeat_tactic 1 9 (((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_mono", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
2010 ];;
2011
2012 (* Lemma leqif_geq *)
2013 let leqif_geq = Sections.section_proof ["m";"n"]
2014 `m <= n ==> leqif m n (n <= m)`
2015 [
2016    ((BETA_TAC THEN (move ["lemn"])) THEN (((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] [])))));
2017    ((((use_arg_then2 ("lemn", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
2018 ];;
2019
2020 (* Lemma leqif_eq *)
2021 let leqif_eq = Sections.section_proof ["m";"n"]
2022 `m <= n ==> leqif m n (m = n)`
2023 [
2024    ((((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
2025 ];;
2026
2027 (* Lemma geq_leqif *)
2028 let geq_leqif = Sections.section_proof ["a";"b";"C"]
2029 `leqif a b C ==> ((b <= a) <=> C)`
2030 [
2031    ((((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] [])))) THEN (case THEN (move ["le_ab"])) THEN (((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] [])))));
2032    ((((use_arg_then2 ("le_ab", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
2033 ];;
2034
2035 (* Lemma ltn_leqif *)
2036 let ltn_leqif = Sections.section_proof ["a";"b";"C"]
2037 `leqif a b C ==> (a < b <=> ~ C)`
2038 [
2039    (BETA_TAC THEN (move ["le_ab"]));
2040    (((((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("geq_leqif", [geq_leqif])) (fun fst_arg -> (use_arg_then2 ("le_ab", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2041 ];;
2042
2043 (* Lemma leqif_add *)
2044 let leqif_add = Sections.section_proof ["m1";"n1";"c1";"m2";"n2";"c2"]
2045 `leqif m1 n1 c1 ==> leqif m2 n2 c2 ==> leqif (m1 + m2) (n1 + n2) (c1 /\ c2)`
2046 [
2047    ((((fun arg_tac -> (use_arg_then2 ("monotone_leqif", [monotone_leqif])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("leq_add2r", [leq_add2r])) (fun fst_arg -> (use_arg_then2 ("m2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["le1"]));
2048    (((fun arg_tac -> (use_arg_then2 ("monotone_leqif", [monotone_leqif])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("leq_add2l", [leq_add2l])) (fun fst_arg -> (use_arg_then2 ("n1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))));
2049    (((use_arg_then2 ("leqif_trans", [leqif_trans])) (disch_tac [])) THEN (clear_assumption "leqif_trans") THEN (exact_tac));
2050 ];;
2051
2052 (* Lemma leqif_mul *)
2053 let leqif_mul = Sections.section_proof ["m1";"n1";"c1";"m2";"n2";"c2"]
2054 `leqif m1 n1 c1 ==> leqif m2 n2 c2 ==>
2055           leqif (m1 * m2) (n1 * n2) (n1 * n2 = 0 \/ (c1 /\ c2))`
2056 [
2057    (BETA_TAC THEN (move ["le1"]) THEN (move ["le2"]));
2058    ((THENL) (((fun arg_tac -> (use_arg_then2 ("posnP", [posnP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n1 * n2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(move ["n12_0"]); ALL_TAC]);
2059    ((((use_arg_then2 ("n12_0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("le2", [])) (disch_tac [])) THEN (clear_assumption "le2") THEN ((use_arg_then2 ("le1", [])) (disch_tac [])) THEN (clear_assumption "le1") THEN ((use_arg_then2 ("n12_0", [])) (disch_tac [])) THEN (clear_assumption "n12_0") THEN BETA_TAC) THEN (((use_arg_then2 ("muln_eq0", [muln_eq0]))(thm_tac (new_rewrite [] [])))));
2060    ((case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((THENL) (((use_arg_then2 ("m2", [])) (disch_tac [])) THEN (clear_assumption "m2") THEN ((use_arg_then2 ("m1", [])) (disch_tac [])) THEN (clear_assumption "m1") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) case [ALL_TAC; (move ["m'"])]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("muln0", [muln0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mul0n", [mul0n]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (arith_tac));
2061    ((((use_arg_then2 ("muln_gt0", [muln_gt0]))(thm_tac (new_rewrite [] [])))) THEN (BETA_TAC THEN (case THEN ((move ["n1_gt0"]) THEN (move ["n2_gt0"])))));
2062    (((fun arg_tac -> (use_arg_then2 ("posnP", [posnP])) (fun fst_arg -> (use_arg_then2 ("m2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN ((THENL) case [(move ["m2_0"]); (move ["m2_gt0"])]));
2063    ((((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("le2", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("leqif", [leqif]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["_"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))))));
2064    (((((use_arg_then2 ("andbC", [andbC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("m2_0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("muln0", [muln0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("muln_gt0", [muln_gt0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n1_gt0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n2_gt0", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2065    ((((use_arg_then2 ("n1_gt0", [])) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("leq_pmul2l", [leq_pmul2l])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("monotone_leqif", [monotone_leqif])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["Mn1"])));
2066    (((use_arg_then2 ("le2", [])) (disch_tac [])) THEN (clear_assumption "le2") THEN ((use_arg_then2 ("Mn1", [])) (disch_tac [])) THEN (clear_assumption "Mn1") THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
2067    ((((use_arg_then2 ("m2_gt0", [])) (disch_tac [])) THEN (clear_assumption "m2_gt0") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("leq_pmul2r", [leq_pmul2r])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("monotone_leqif", [monotone_leqif])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["Mm2"])));
2068    (((use_arg_then2 ("le1", [])) (disch_tac [])) THEN (clear_assumption "le1") THEN ((use_arg_then2 ("Mm2", [])) (disch_tac [])) THEN (clear_assumption "Mm2") THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
2069    (BETA_TAC THEN (move ["leq1"]) THEN (move ["leq2"]));
2070    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leqif_trans", [leqif_trans])) (fun fst_arg -> (use_arg_then2 ("leq1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("leq2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] []))))));
2071    (((fun arg_tac -> arg_tac (Arg_term (`c1 /\ c2`))) (disch_tac [])) THEN case THEN (simp_tac));
2072    (((((use_arg_then2 ("eqn_leq", [eqn_leq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("muln_gt0", [muln_gt0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n1_gt0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n2_gt0", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2073 ];;
2074
2075 (* Lemma nat_Cauchy *)
2076 let nat_Cauchy = Sections.section_proof ["m";"n"]
2077 `leqif (2 * (m * n)) (m ^ 2 + n ^ 2) (m = n)`
2078 [
2079    ((fun arg_tac -> arg_tac (Arg_term (`n <= m`))) (term_tac (wlog_tac (move ["le_nm"])[`m`; `n`])));
2080    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leqP", [leqP])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN ((TRY done_tac))) THEN (((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulnC", [mulnC]))(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (move ["mn"])));
2081    ((((use_arg_then2 ("le_nm", [])) (disch_tac [])) THEN (clear_assumption "le_nm") THEN (DISCH_THEN apply_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("ltnW", [ltnW])) (fun fst_arg -> (use_arg_then2 ("mn", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
2082    (BETA_TAC THEN (move ["le_nm"]));
2083    (((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] []))));
2084    ((THENL_FIRST) ((THENL) (((fun arg_tac -> (use_arg_then2 ("EXCLUDED_MIDDLE", [EXCLUDED_MIDDLE])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m = n`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); (move ["ne_mn"])]) (((((use_arg_then2 ("mulnn", [mulnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnn", [addnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mul2n", [mul2n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
2085    (((((use_arg_then2 ("ne_mn", []))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac)) THEN ((((use_arg_then2 ("subn_gt0", [subn_gt0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sqrn_sub", [sqrn_sub]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("sqrn_gt0", [sqrn_gt0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("subn_gt0", [subn_gt0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltn_neqAle", [ltn_neqAle]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2086 ];;
2087
2088 (* Lemma nat_AGM2 *)
2089 let nat_AGM2 = Sections.section_proof ["m";"n"]
2090 `leqif (4 * (m * n)) ((m + n) ^ 2) (m = n)`
2091 [
2092    ((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `4 = 2 * 2`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mulnA", [mulnA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mul2n", [mul2n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addnn", [addnn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sqrn_add", [sqrn_add]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] [])))));
2093    ((((use_arg_then2 ("ltn_add2r", [ltn_add2r]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqn_addr", [eqn_addr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltn_neqAle", [ltn_neqAle]))(thm_tac (new_rewrite [] [])))));
2094    (((((fun arg_tac -> (use_arg_then2 ("leqif_imp_eq", [leqif_imp_eq])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nat_Cauchy", [nat_Cauchy])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("leqif_imp_le", [leqif_imp_le])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nat_Cauchy", [nat_Cauchy])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("if_same", [if_same]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2095 ];;
2096 let distn = new_definition `!m n. distn m n = (m - n) + (n - m)`;;
2097
2098 (* Lemma distnC *)
2099 let distnC = Sections.section_proof ["m";"n"]
2100 `distn m n = distn n m`
2101 [
2102    (((repeat_tactic 1 9 (((use_arg_then2 ("distn", [distn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2103 ];;
2104
2105 (* Lemma distn_add2l *)
2106 let distn_add2l = Sections.section_proof ["d";"m";"n"]
2107 `distn (d + m) (d + n) = distn m n`
2108 [
2109    (((repeat_tactic 1 9 (((use_arg_then2 ("distn", [distn]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("subn_add2l", [subn_add2l]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
2110 ];;
2111
2112 (* Lemma distn_add2r *)
2113 let distn_add2r = Sections.section_proof ["d";"m";"n"]
2114 `distn (m + d) (n + d) = distn m n`
2115 [
2116    (((repeat_tactic 1 9 (((use_arg_then2 ("distn", [distn]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("subn_add2r", [subn_add2r]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
2117 ];;
2118
2119 (* Lemma distnEr *)
2120 let distnEr = Sections.section_proof ["m";"n"]
2121 `m <= n ==> distn m n = n - m`
2122 [
2123    (BETA_TAC THEN (move ["le_m_n"]));
2124    (((((use_arg_then2 ("distn", [distn]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("EQ_IMP", [EQ_IMP])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leqE", [leqE])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("le_m_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2125 ];;
2126
2127 (* Lemma distnEl *)
2128 let distnEl = Sections.section_proof ["m";"n"]
2129 `n <= m ==> distn m n = m - n`
2130 [
2131    ((BETA_TAC THEN (move ["le_n_m"])) THEN ((((use_arg_then2 ("distnC", [distnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("distnEr", [distnEr]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2132 ];;
2133
2134 (* Lemma dist0n *)
2135 let dist0n = Sections.section_proof ["n"]
2136 `distn 0 n = n`
2137 [
2138    (((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["m"])]) THEN ((((use_arg_then2 ("distn", [distn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("sub0n", [sub0n]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("subn0", [subn0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2139 ];;
2140
2141 (* Lemma distn0 *)
2142 let distn0 = Sections.section_proof ["n"]
2143 `distn n 0 = n`
2144 [
2145    (((((use_arg_then2 ("distnC", [distnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dist0n", [dist0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2146 ];;
2147
2148 (* Lemma distnn *)
2149 let distnn = Sections.section_proof ["m"]
2150 `distn m m = 0`
2151 [
2152    (((repeat_tactic 1 9 (((use_arg_then2 ("distn", [distn]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("subnn", [subnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2153 ];;
2154
2155 (* Lemma distn_eq0 *)
2156 let distn_eq0 = Sections.section_proof ["m";"n"]
2157 `(distn m n = 0) <=> (m = n)`
2158 [
2159    (((((use_arg_then2 ("distn", [distn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn_eq0", [addn_eq0]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("subn_eq0", [subn_eq0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqn_leq", [eqn_leq]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
2160 ];;
2161
2162 (* Lemma distnS *)
2163 let distnS = Sections.section_proof ["m"]
2164 `distn m (SUC m) = 1`
2165 [
2166    ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("distn_add2r", [distn_add2r])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dist0n", [dist0n]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2167 ];;
2168
2169 (* Lemma distSn *)
2170 let distSn = Sections.section_proof ["m"]
2171 `distn (SUC m) m = 1`
2172 [
2173    (((((use_arg_then2 ("distnC", [distnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("distnS", [distnS]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2174 ];;
2175
2176 (* Lemma distn_eq1 *)
2177 let distn_eq1 = Sections.section_proof ["m";"n"]
2178 `(distn m n = 1) <=> (if m < n then SUC m = n else m = SUC n)`
2179 [
2180    ((THENL) (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ltnP", [ltnP])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(move ["lt_mn"]); (move ["le_mn"])]);
2181    (((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [(`_ = 1`)])))) THEN (((fun arg_tac -> (use_arg_then2 ("eqn_addr", [eqn_addr])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("distnEr", [distnEr]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ltnW", [ltnW]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2182    (((((fun arg_tac -> (use_arg_then2 ("eqn_addr", [eqn_addr])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("distnEl", [distnEl]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("add1n", [add1n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("le_mn", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
2183 ];;
2184
2185 (* Lemma leqif_add_distn *)
2186 let leqif_add_distn = Sections.section_proof ["m";"n";"p"]
2187 `leqif (distn m p) (distn m n + distn n p) ((m <= n /\ n <= p) \/ (p <= n /\ n <= m))`
2188 [
2189    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`!m p. m <= p ==> leqif (distn m p) (distn m n + distn n p) (m <= n /\ n <= p \/ p <= n /\ n <= m)`))) (term_tac (have_gen_tac [](move ["IH"])))));
2190    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leq_total", [leq_total])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("p", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN ((TRY done_tac))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("IH", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC));
2191    (((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbC", [orbC]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("distnC", [distnC])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`distn n _`)])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("distnC", [distnC]))(thm_tac (new_rewrite [] [(`distn p _`)])))))) THEN (done_tac));
2192    (BETA_TAC THEN (move ["m"]) THEN (move ["p"]) THEN (move ["le_mp"]));
2193    ((((use_arg_then2 ("distnEr", [distnEr]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
2194    ((THENL) (((fun arg_tac -> (use_arg_then2 ("EXCLUDED_MIDDLE", [EXCLUDED_MIDDLE])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`m <= n /\ n <= p`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [((case THEN ((move ["le_mn"]) THEN (move ["le_np"]))) THEN ((simp_tac THEN TRY done_tac))); ALL_TAC]);
2195    (((repeat_tactic 1 9 (((use_arg_then2 ("distnEr", [distnEr]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((fun arg_tac -> (use_arg_then2 ("eqn_addr", [eqn_addr])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnA", [addnA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
2196    (((((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ltnNge", [ltnNge]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN ALL_TAC THEN ((THENL) case [(move ["lt_nm"]); (move ["lt_pn"])]));
2197    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ltn_leq_trans", [ltn_leq_trans])) (fun fst_arg -> (use_arg_then2 ("lt_nm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("le_mp", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["lt_np"]));
2198    (((((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lt_nm", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lt_np", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ltn_addl", [ltn_addl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("distnEr", [distnEr]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ltnW", [ltnW]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ltn_sub2l", [ltn_sub2l]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2199    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leq_ltn_trans", [leq_ltn_trans])) (fun fst_arg -> (use_arg_then2 ("le_mp", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("lt_pn", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["lt_mn"]));
2200    (((((use_arg_then2 ("leqifP", [leqifP]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lt_mn", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lt_pn", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ltn_addr", [ltn_addr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("distnEr", [distnEr]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ltn_sub2r", [ltn_sub2r]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ltnW", [ltnW]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2201 ];;
2202
2203 (* Lemma leq_add_distn *)
2204 let leq_add_distn = Sections.section_proof ["m";"n";"p"]
2205 `distn m p <= distn m n + distn n p`
2206 [
2207    ((((fun arg_tac -> (use_arg_then2 ("leqif_imp_le", [leqif_imp_le])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leqif_add_distn", [leqif_add_distn])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("p", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
2208 ];;
2209
2210 (* Lemma sqrn_distn *)
2211 let sqrn_distn = Sections.section_proof ["m";"n"]
2212 `(distn m n) ^ 2 + 2 * (m * n) = m ^ 2 + n ^ 2`
2213 [
2214    ((fun arg_tac -> arg_tac (Arg_term (`n <= m`))) (term_tac (wlog_tac (move ["le_nm"])[`m`; `n`])));
2215    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leq_total", [leq_total])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("le_nm", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN ((TRY done_tac)));
2216    (((((fun arg_tac -> (use_arg_then2 ("addnC", [addnC])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`n EXP 2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("mulnC", [mulnC])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("distnC", [distnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2217    ((BETA_TAC THEN (move ["le_nm"])) THEN ((((use_arg_then2 ("distnEl", [distnEl]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("sqrn_sub", [sqrn_sub]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("leqif_imp_le", [leqif_imp_le])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nat_Cauchy", [nat_Cauchy])) (fun fst_arg -> (use_arg_then2 ("m", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
2218 ];;
2219
2220 (* Close the module *)
2221 end;;