formal_ineqs/lib/ssrnat-compiled.hl

   1 needs "lib/ssrbool-compiled.hl";;
   2 prioritize_num();;
   3
   4 (* Lemma succnK *)
   5 let succnK = section_proof ["n"] `SUC n - 1 = n` [
   6    ((arith_tac) THEN (done_tac));
   7 ];;
   8
   9 (* Lemma succn_inj *)
  10 let succn_inj = section_proof ["n";"m"] `SUC n = SUC m ==> n = m` [
  11    ((arith_tac) THEN (done_tac));
  12 ];;
  13
  14 (* Lemma eqSS *)
  15 let eqSS = section_proof ["m";"n"] `(SUC m = SUC n) = (m = n)` [
  16    ((arith_tac) THEN (done_tac));
  17 ];;
  18
  19 (* Lemma add0n *)
  20 let add0n = section_proof ["n"] `0 + n = n` [
  21    ((arith_tac) THEN (done_tac));
  22 ];;
  23
  24 (* Lemma addSn *)
  25 let addSn = section_proof ["m";"n"] `SUC m + n = SUC (m + n)` [
  26    ((arith_tac) THEN (done_tac));
  27 ];;
  28
  29 (* Lemma add1n *)
  30 let add1n = section_proof ["n"] `1 + n = SUC n` [
  31    ((arith_tac) THEN (done_tac));
  32 ];;
  33
  34 (* Lemma addn0 *)
  35 let addn0 = section_proof ["n"] `n + 0 = n` [
  36    ((arith_tac) THEN (done_tac));
  37 ];;
  38
  39 (* Lemma addnS *)
  40 let addnS = section_proof ["m";"n"] `m + SUC n = SUC (m + n)` [
  41    ((arith_tac) THEN (done_tac));
  42 ];;
  43
  44 (* Lemma addSnnS *)
  45 let addSnnS = section_proof ["m";"n"] `SUC m + n = m + SUC n` [
  46    ((arith_tac) THEN (done_tac));
  47 ];;
  48
  49 (* Lemma addnCA *)
  50 let addnCA = section_proof ["m";"n";"p"] `m + (n + p) = n + (m + p)` [
  51    ((arith_tac) THEN (done_tac));
  52 ];;
  53
  54 (* Lemma addnC *)
  55 let addnC = section_proof ["m";"n"] `m + n = n + m` [
  56    (((((fun arg_tac -> (use_arg_then "addn0") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  57 ];;
  58
  59 (* Lemma addn1 *)
  60 let addn1 = section_proof ["n"] `n + 1 = SUC n` [
  61    (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  62 ];;
  63
  64 (* Lemma addnA *)
  65 let addnA = section_proof ["n";"m";"p"] `n + (m + p) = (n + m) + p` [
  66    (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`m + p`)])))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  67 ];;
  68
  69 (* Lemma addnAC *)
  70 let addnAC = section_proof ["m";"n";"p"] `(n + m) + p = (n + p) + m` [
  71    (((repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`p + m`)]))))) THEN (done_tac));
  72 ];;
  73
  74 (* Lemma addn_eq0 *)
  75 let addn_eq0 = section_proof ["m";"n"] `(m + n = 0) <=> (m = 0) /\ (n = 0)` [
  76    ((arith_tac) THEN (done_tac));
  77 ];;
  78
  79 (* Lemma eqn_addl *)
  80 let eqn_addl = section_proof ["p";"m";"n"] `(p + m = p + n) <=> (m = n)` [
  81    ((arith_tac) THEN (done_tac));
  82 ];;
  83
  84 (* Lemma eqn_addr *)
  85 let eqn_addr = section_proof ["p";"m";"n"] `(m + p = n + p) = (m = n)` [
  86    ((arith_tac) THEN (done_tac));
  87 ];;
  88
  89 (* Lemma addnI *)
  90 let addnI = section_proof ["m";"n1";"n2"] `m + n1 = m + n2 ==> n1 = n2` [
  91    ((BETA_TAC THEN (move ["Heq"])) THEN (((fun arg_tac -> (use_arg_then "eqn_addl") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
  92 ];;
  93
  94 (* Lemma addIn *)
  95 let addIn = section_proof ["m";"n1";"n2"] `n1 + m = n2 + m ==> n1 = n2` [
  96    ((repeat_tactic 1 9 (((use_arg_then "addnC")(gsym_then (thm_tac (new_rewrite [] [(`_1 + m`)])))))) THEN (move ["Heq"]));
  97    ((((fun arg_tac -> (use_arg_then "addnI") (fun fst_arg -> (use_arg_then "Heq") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
  98 ];;
  99
 100 (* Lemma sub0n *)
 101 let sub0n = section_proof ["n"] `0 - n = 0` [
 102    ((arith_tac) THEN (done_tac));
 103 ];;
 104
 105 (* Lemma subn0 *)
 106 let subn0 = section_proof ["n"] `n - 0 = n` [
 107    ((arith_tac) THEN (done_tac));
 108 ];;
 109
 110 (* Lemma subnn *)
 111 let subnn = section_proof [] `!n. n - n = 0` [
 112    ((arith_tac) THEN (done_tac));
 113 ];;
 114
 115 (* Lemma subSS *)
 116 let subSS = section_proof [] `!n m. SUC m - SUC n = m - n` [
 117    ((arith_tac) THEN (done_tac));
 118 ];;
 119
 120 (* Lemma subn_add2l *)
 121 let subn_add2l = section_proof [] `!p m n. (p + m) - (p + n) = m - n` [
 122    ((arith_tac) THEN (done_tac));
 123 ];;
 124
 125 (* Lemma subn_add2r *)
 126 let subn_add2r = section_proof [] `!p m n. (m + p) - (n + p) = m - n` [
 127    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 128    (((repeat_tactic 1 9 (((use_arg_then "addnC")(gsym_then (thm_tac (new_rewrite [] [(`_1 + p`)])))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 129 ];;
 130
 131 (* Lemma addKn *)
 132 let addKn = section_proof ["n"] `!x. (n + x) - n = x` [
 133    ((BETA_TAC THEN (move ["m"])) THEN ((((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [2] [(`n`)]))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 134 ];;
 135
 136 (* Lemma addnK *)
 137 let addnK = section_proof [] `!n x. (x + n) - n = x` [
 138    ((BETA_TAC THEN (move ["n"]) THEN (move ["m"])) THEN ((((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addKn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 139 ];;
 140
 141 (* Lemma subSnn *)
 142 let subSnn = section_proof ["n"] `SUC n - n = 1` [
 143    (((((use_arg_then "add1n")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 144 ];;
 145
 146 (* Lemma subn_sub *)
 147 let subn_sub = section_proof ["m";"n";"p"] `(n - m) - p = n - (m + p)` [
 148    ((arith_tac) THEN (done_tac));
 149 ];;
 150
 151 (* Lemma subnAC *)
 152 let subnAC = section_proof [] `!m n p. (m - n) - p = (m - p) - n` [
 153    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then "subn_sub")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 154 ];;
 155
 156 (* Lemma predn_sub *)
 157 let predn_sub = section_proof [] `!m n. (m - n) - 1 = m - SUC n` [
 158    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN ((((use_arg_then "subn_sub")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn1")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 159 ];;
 160
 161 (* Lemma predn_subS *)
 162 let predn_subS = section_proof [] `!m n. (SUC m - n) - 1 = m - n` [
 163    (((((use_arg_then "predn_sub")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 164 ];;
 165
 166 (* Lemma ltnS *)
 167 let ltnS = section_proof [] `!m n. (m < SUC n) = (m <= n)` [
 168    ((arith_tac) THEN (done_tac));
 169 ];;
 170
 171 (* Lemma leq0n *)
 172 let leq0n = section_proof [] `!n. 0 <= n` [
 173    ((arith_tac) THEN (done_tac));
 174 ];;
 175
 176 (* Lemma ltn0Sn *)
 177 let ltn0Sn = section_proof [] `!n. 0 < SUC n` [
 178    ((arith_tac) THEN (done_tac));
 179 ];;
 180
 181 (* Lemma ltn0 *)
 182 let ltn0 = section_proof [] `!n. n < 0 <=> F` [
 183    ((arith_tac) THEN (done_tac));
 184 ];;
 185
 186 (* Lemma leqnn *)
 187 let leqnn = section_proof [] `!n. n <= n` [
 188    ((arith_tac) THEN (done_tac));
 189 ];;
 190
 191 (* Lemma ltnSn *)
 192 let ltnSn = section_proof [] `!n. n < SUC n` [
 193    ((arith_tac) THEN (done_tac));
 194 ];;
 195
 196 (* Lemma eq_leq *)
 197 let eq_leq = section_proof [] `!m n. m = n ==> m <= n` [
 198    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 199 ];;
 200
 201 (* Lemma leqnSn *)
 202 let leqnSn = section_proof [] `!n. n <= SUC n` [
 203    ((arith_tac) THEN (done_tac));
 204 ];;
 205
 206 (* Lemma leq_pred *)
 207 let leq_pred = section_proof [] `!n. n - 1 <= n` [
 208    ((arith_tac) THEN (done_tac));
 209 ];;
 210
 211 (* Lemma leqSpred *)
 212 let leqSpred = section_proof [] `!n. n <= SUC (n - 1)` [
 213    ((arith_tac) THEN (done_tac));
 214 ];;
 215
 216 (* Lemma ltn_predK *)
 217 let ltn_predK = section_proof [] `!m n. m < n ==> SUC (n - 1) = n` [
 218    ((arith_tac) THEN (done_tac));
 219 ];;
 220
 221 (* Lemma prednK *)
 222 let prednK = section_proof [] `!n. 0 < n ==> SUC (n - 1) = n` [
 223    ((BETA_TAC THEN (move ["n"]) THEN (move ["H"])) THEN (((fun arg_tac -> (use_arg_then "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)));
 224 ];;
 225
 226 (* Lemma leqNgt *)
 227 let leqNgt = section_proof [] `!m n. (m <= n) <=> ~(n < m)` [
 228    ((arith_tac) THEN (done_tac));
 229 ];;
 230
 231 (* Lemma ltnNge *)
 232 let ltnNge = section_proof [] `!m n. (m < n) = ~(n <= m)` [
 233    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 234 ];;
 235
 236 (* Lemma ltnn *)
 237 let ltnn = section_proof [] `!n. n < n <=> F` [
 238    ((BETA_TAC THEN (move ["n"])) THEN ((((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 239 ];;
 240
 241 (* Lemma leqn0 *)
 242 let leqn0 = section_proof [] `!n. (n <= 0) = (n = 0)` [
 243    ((arith_tac) THEN (done_tac));
 244 ];;
 245
 246 (* Lemma lt0n *)
 247 let lt0n = section_proof [] `!n. (0 < n) = ~(n = 0)` [
 248    ((arith_tac) THEN (done_tac));
 249 ];;
 250
 251 (* Lemma lt0n_neq0 *)
 252 let lt0n_neq0 = section_proof [] `!n. 0 < n ==> ~(n = 0)` [
 253    ((arith_tac) THEN (done_tac));
 254 ];;
 255
 256 (* Lemma eqn0Ngt *)
 257 let eqn0Ngt = section_proof [] `!n. (n = 0) = ~(0 < n)` [
 258    ((arith_tac) THEN (done_tac));
 259 ];;
 260
 261 (* Lemma neq0_lt0n *)
 262 let neq0_lt0n = section_proof [] `!n. (n = 0) = F ==> 0 < n` [
 263    ((arith_tac) THEN (done_tac));
 264 ];;
 265
 266 (* Lemma eqn_leq *)
 267 let eqn_leq = section_proof [] `!m n. (m = n) = (m <= n /\ n <= m)` [
 268    ((arith_tac) THEN (done_tac));
 269 ];;
 270
 271 (* Lemma anti_leq *)
 272 let anti_leq = section_proof [] `!m n. m <= n /\ n <= m ==> m = n` [
 273    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 274 ];;
 275
 276 (* Lemma neq_ltn *)
 277 let neq_ltn = section_proof [] `!m n. ~(m = n) <=> (m < n) \/ (n < m)` [
 278    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 279    (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_and")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 280 ];;
 281
 282 (* Lemma leq_eqVlt *)
 283 let leq_eqVlt = section_proof ["m";"n"] `(m <= n) <=> (m = n) \/ (m < n)` [
 284    ((arith_tac) THEN (done_tac));
 285 ];;
 286
 287 (* Lemma eq_sym *)
 288 let eq_sym = section_proof [] `!x y:A. x = y <=> y = x` [
 289    ((((use_arg_then "EQ_SYM_EQ") (disch_tac [])) THEN (clear_assumption "EQ_SYM_EQ") THEN BETA_TAC) THEN (done_tac));
 290 ];;
 291
 292 (* Lemma ltn_neqAle *)
 293 let ltn_neqAle = section_proof [] `!m n. (m < n) <=> ~(m = n) /\ (m <= n)` [
 294    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 295    (((((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_eqVlt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`n = m`)]))))) THEN (done_tac));
 296 ];;
 297
 298 (* Lemma leq_trans *)
 299 let leq_trans = section_proof [] `!n m p. m <= n ==> n <= p ==> m <= p` [
 300    ((arith_tac) THEN (done_tac));
 301 ];;
 302
 303 (* Lemma ltE *)
 304 let ltE = section_proof [] `!n m. n < m <=> SUC n <= m` [
 305    ((arith_tac) THEN (done_tac));
 306 ];;
 307
 308 (* Lemma leqSS *)
 309 let leqSS = section_proof [] `!n m. SUC n <= SUC m <=> n <= m` [
 310    ((arith_tac) THEN (done_tac));
 311 ];;
 312
 313 (* Lemma leq_ltn_trans *)
 314 let leq_ltn_trans = section_proof [] `!n m p. m <= n ==> n < p ==> m < p` [
 315    (BETA_TAC THEN (move ["n"]) THEN (move ["m"]) THEN (move ["p"]) THEN (move ["Hmn"]));
 316    (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] [])))) THEN (done_tac)) THEN (done_tac));
 317 ];;
 318
 319 (* Lemma ltn_leq_trans *)
 320 let ltn_leq_trans = section_proof ["n";"m";"p"] `m < n ==> n <= p ==> m < p` [
 321    ((arith_tac) THEN (done_tac));
 322 ];;
 323
 324 (* Lemma ltnW *)
 325 let ltnW = section_proof [] `!m n. m < n ==> m <= n` [
 326    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "leqnSn")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 327 ];;
 328
 329 (* Lemma leqW *)
 330 let leqW = section_proof [] `!m n. m <= n ==> m <= SUC n` [
 331    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["le_mn"])) THEN (((use_arg_then "ltnW") (disch_tac [])) THEN (clear_assumption "ltnW") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 332 ];;
 333
 334 (* Lemma ltn_trans *)
 335 let ltn_trans = section_proof [] `!n m p. m < n ==> n < p ==> m < p` [
 336    (BETA_TAC THEN (move ["n"]) THEN (move ["m"]) THEN (move ["p"]) THEN (move ["lt_mn"]));
 337    (((DISCH_THEN (fun snd_th -> (use_arg_then "ltnW") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))));
 338    ((((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 339 ];;
 340
 341 (* Lemma geqE *)
 342 let geqE = section_proof [] `!m n. m >= n <=> n <= m` [
 343    ((arith_tac) THEN (done_tac));
 344 ];;
 345
 346 (* Lemma gtE *)
 347 let gtE = section_proof ["m";"n"] `m > n <=> n < m` [
 348    (arith_tac);
 349 ];;
 350
 351 (* Lemma leq_total *)
 352 let leq_total = section_proof ["m";"n"] `(m <= n) \/ (n <= m)` [
 353    ((((((use_arg_then "implyNb")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "ltnNge")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["lt_nm"])) THEN (((use_arg_then "ltnW") (disch_tac [])) THEN (clear_assumption "ltnW") THEN (exact_tac)) THEN (done_tac));
 354 ];;
 355
 356 (* Lemma leqP *)
 357 let leqP = section_proof ["m";"n"] `m <= n \/ n < m` [
 358    ((arith_tac) THEN (done_tac));
 359 ];;
 360
 361 (* Lemma ltnP *)
 362 let ltnP = section_proof ["m";"n"] `m < n \/ n <= m` [
 363    ((arith_tac) THEN (done_tac));
 364 ];;
 365
 366 (* Lemma posnP *)
 367 let posnP = section_proof ["n"] `n = 0 \/ 0 < n` [
 368    ((arith_tac) THEN (done_tac));
 369 ];;
 370
 371 (* Lemma ltngtP *)
 372 let ltngtP = section_proof ["m";"n"] `m < n \/ n < m \/ m = n` [
 373    ((arith_tac) THEN (done_tac));
 374 ];;
 375
 376 (* Lemma leq_add2l *)
 377 let leq_add2l = section_proof [] `!p m n. (p + m <= p + n) = (m <= n)` [
 378    ((arith_tac) THEN (done_tac));
 379 ];;
 380
 381 (* Lemma ltn_add2l *)
 382 let ltn_add2l = section_proof [] `!p m n. (p + m < p + n) = (m < n)` [
 383    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 384    (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnS")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 385 ];;
 386
 387 (* Lemma leq_add2r *)
 388 let leq_add2r = section_proof ["p";"m";"n"] `(m + p <= n + p) = (m <= n)` [
 389    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "p") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "leq_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 390 ];;
 391
 392 (* Lemma ltn_add2r *)
 393 let ltn_add2r = section_proof [] `!p m n. (m + p < n + p) = (m < n)` [
 394    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 395    (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addSn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_add2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 396 ];;
 397
 398 (* Lemma leq_add *)
 399 let leq_add = section_proof [] `!m1 m2 n1 n2. m1 <= n1 ==> m2 <= n2 ==> m1 + m2 <= n1 + n2` [
 400    (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n1"]) THEN (move ["n2"]) THEN (move ["le_mn1"]) THEN (move ["le_mn2"]));
 401    (((((fun arg_tac -> (use_arg_then "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_then "leq_add2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_add2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 402 ];;
 403
 404 (* Lemma leq_addr *)
 405 let leq_addr = section_proof [] `!m n. n <= n + m` [
 406    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 407    (((((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [1] [(`n`)]))))) THEN (((use_arg_then "leq_add2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 408 ];;
 409
 410 (* Lemma leq_addl *)
 411 let leq_addl = section_proof [] `!m n. n <= m + n` [
 412    (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addr")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 413 ];;
 414
 415 (* Lemma ltn_addr *)
 416 let ltn_addr = section_proof ["m";"n";"p"] `m < n ==> m < n + p` [
 417    ((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "leq_addr")(thm_tac (new_rewrite [] [])))));
 418 ];;
 419
 420 (* Lemma ltn_addl *)
 421 let ltn_addl = section_proof [] `!m n p. m < n ==> m < p + n` [
 422    ((arith_tac) THEN (done_tac));
 423 ];;
 424
 425 (* Lemma addn_gt0 *)
 426 let addn_gt0 = section_proof [] `!m n. (0 < m + n) <=> (0 < m) \/ (0 < n)` [
 427    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 428    (((repeat_tactic 1 9 (((use_arg_then "lt0n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "negb_and")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addn_eq0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 429 ];;
 430
 431 (* Lemma subn_gt0 *)
 432 let subn_gt0 = section_proof ["m";"n"] `(0 < n - m) = (m < n)` [
 433    ((arith_tac) THEN (done_tac));
 434 ];;
 435
 436 (* Lemma subn_eq0 *)
 437 let subn_eq0 = section_proof [] `!m n. (m - n = 0) = (m <= n)` [
 438    ((arith_tac) THEN (done_tac));
 439 ];;
 440
 441 (* Lemma leqE *)
 442 let leqE = section_proof [] `!m n. m <= n <=> m - n = 0` [
 443    ((arith_tac) THEN (done_tac));
 444 ];;
 445
 446 (* Lemma leq_sub_add *)
 447 let leq_sub_add = section_proof [] `!m n p. (m - n <= p) = (m <= n + p)` [
 448    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 449    (((((use_arg_then "subn_eq0")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_sub")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 450 ];;
 451
 452 (* Lemma leq_subr *)
 453 let leq_subr = section_proof [] `!m n. n - m <= n` [
 454    (((((use_arg_then "leq_sub_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 455 ];;
 456
 457 (* Lemma subnKC *)
 458 let subnKC = section_proof [] `!m n. m <= n ==> m + (n - m) = n` [
 459    ((arith_tac) THEN (done_tac));
 460 ];;
 461
 462 (* Lemma subnK *)
 463 let subnK = section_proof [] `!m n. m <= n ==> (n - m) + m = n` [
 464    ((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subnKC") (disch_tac [])) THEN (clear_assumption "subnKC") THEN (exact_tac)) THEN (done_tac));
 465 ];;
 466
 467 (* Lemma addn_subA *)
 468 let addn_subA = section_proof [] `!m n p. p <= n ==> m + (n - p) = (m + n) - p` [
 469    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]) THEN (move ["le_pn"]));
 470    (((((fun arg_tac -> (use_arg_then "subnK") (fun fst_arg -> (use_arg_then "le_pn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 471 ];;
 472
 473 (* Lemma subn_subA *)
 474 let subn_subA = section_proof [] `!m n p. p <= n ==> m - (n - p) = (m + p) - n` [
 475    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]) THEN (move ["le_pn"]));
 476    (((((fun arg_tac -> (use_arg_then "subnK") (fun fst_arg -> (use_arg_then "le_pn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 477 ];;
 478
 479 (* Lemma subKn *)
 480 let subKn = section_proof [] `!m n. m <= n ==> n - (n - m) = m` [
 481    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 482    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "subn_subA") (fun fst_arg -> (use_arg_then "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_then "addKn")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 483 ];;
 484
 485 (* Lemma leq_subS *)
 486 let leq_subS = section_proof [] `!m n. m <= n ==> SUC n - m = SUC (n - m)` [
 487    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 488    ((((use_arg_then "add1n")(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "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 [] [])))))));
 489    ((((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 490 ];;
 491
 492 (* Lemma ltn_subS *)
 493 let ltn_subS = section_proof [] `!m n. m < n ==> n - m = SUC (n - SUC m)` [
 494    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["lt_mn"])) THEN ((((use_arg_then "leq_subS")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 495 ];;
 496
 497 (* Lemma leq_sub2r *)
 498 let leq_sub2r = section_proof [] `!p m n. m <= n ==> m - p <= n - p` [
 499    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]) THEN (move ["le_mn"]));
 500    (((((use_arg_then "leq_sub_add")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "leq_trans") (fun fst_arg -> (use_arg_then "le_mn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_sub_add")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 501 ];;
 502
 503 (* Lemma leq_sub2l *)
 504 let leq_sub2l = section_proof [] `!p m n. m <= n ==> p - n <= p - m` [
 505    ((BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"])) THEN ((((fun arg_tac -> (use_arg_then "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_then "leq_sub_add")(thm_tac (new_rewrite [] []))))));
 506    ((((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then "leq_sub_add")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 507 ];;
 508
 509 (* Lemma leq_sub2 *)
 510 let leq_sub2 = section_proof [] `!m1 m2 n1 n2. m1 <= m2 ==> n2 <= n1 ==> m1 - n1 <= m2 - n2` [
 511    (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n1"]) THEN (move ["n2"]));
 512    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_sub2r") (fun fst_arg -> (use_arg_then "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_then "leq_sub2l") (fun fst_arg -> (use_arg_then "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_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (exact_tac)));
 513 ];;
 514
 515 (* Lemma ltn_sub2r *)
 516 let ltn_sub2r = section_proof [] `!p m n. p < n ==> m < n ==> m - p < n - p` [
 517    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 518    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] []))))));
 519    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "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_then "subSS")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 520 ];;
 521
 522 (* Lemma ltn_sub2l *)
 523 let ltn_sub2l = section_proof [] `!p m n. m < p ==> m < n ==> p - n < p - m` [
 524    (BETA_TAC THEN (move ["p"]) THEN (move ["m"]) THEN (move ["n"]));
 525    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] []))))));
 526    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_sub2l") (fun fst_arg -> (use_arg_then "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));
 527 ];;
 528
 529 (* Lemma ltn_add_sub *)
 530 let ltn_add_sub = section_proof [] `!m n p. (m + n < p) = (n < p - m)` [
 531    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 532    (((repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_sub_add")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 533 ];;
 534 let maxn = new_definition `maxn m n = if m < n then n else m`;;
 535 let minn = new_definition `minn m n = if m < n then m else n`;;
 536
 537 (* Lemma max0n *)
 538 let max0n = section_proof [] `!n. maxn 0 n = n` [
 539    ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 540 ];;
 541
 542 (* Lemma maxn0 *)
 543 let maxn0 = section_proof [] `!n. maxn n 0 = n` [
 544    ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 545 ];;
 546
 547 (* Lemma maxnC *)
 548 let maxnC = section_proof [] `!m n. maxn m n = maxn n m` [
 549    ((repeat_tactic 1 9 (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
 550 ];;
 551
 552 (* Lemma maxnl *)
 553 let maxnl = section_proof [] `!m n. n <= m ==> maxn m n = m` [
 554    ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 555 ];;
 556
 557 (* Lemma maxnr *)
 558 let maxnr = section_proof [] `!m n. m <= n ==> maxn m n = n` [
 559    ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 560 ];;
 561
 562 (* Lemma add_sub_maxn *)
 563 let add_sub_maxn = section_proof [] `!m n. m + (n - m) = maxn m n` [
 564    ((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 565 ];;
 566
 567 (* Lemma maxnAC *)
 568 let maxnAC = section_proof [] `!m n p. maxn (maxn m n) p = maxn (maxn m p) n` [
 569    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 570    (((repeat_tactic 1 9 (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_sub")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "add_sub_maxn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 571 ];;
 572
 573 (* Lemma maxnA *)
 574 let maxnA = section_proof [] `!m n p. maxn m (maxn n p) = maxn (maxn m n) p` [
 575    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 576    (((repeat_tactic 1 9 (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (((use_arg_then "maxnAC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 577 ];;
 578
 579 (* Lemma maxnCA *)
 580 let maxnCA = section_proof [] `!m n p. maxn m (maxn n p) = maxn n (maxn m p)` [
 581    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then "maxnA")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (done_tac));
 582 ];;
 583
 584 (* Lemma eqn_maxr *)
 585 let eqn_maxr = section_proof [] `!m n. (maxn m n = n) = (m <= n)` [
 586    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 587    (((((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [2] [(`n`)]))))) THEN (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 588 ];;
 589
 590 (* Lemma eqn_maxl *)
 591 let eqn_maxl = section_proof [] `!m n. (maxn m n = m) = (n <= m)` [
 592    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 593    (((((use_arg_then "addn0")(gsym_then (thm_tac (new_rewrite [2] [(`m`)]))))) THEN (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 594 ];;
 595
 596 (* Lemma maxnn *)
 597 let maxnn = section_proof [] `!n. maxn n n = n` [
 598    (BETA_TAC THEN (move ["n"]));
 599    (((((use_arg_then "maxnl")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 600 ];;
 601
 602 (* Lemma leq_maxr *)
 603 let leq_maxr = section_proof ["m";"n1";"n2"] `(m <= maxn n1 n2) <=> (m <= n1) \/ (m <= n2)` [
 604    ((fun arg_tac -> arg_tac (Arg_term (`n2 <= n1`))) (term_tac (wlog_tac (move ["le_n21"])[`n1`; `n2`])));
 605    (((THENL_LAST) (((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_total") (fun fst_arg -> (use_arg_then "n2") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (move ["le_n12"])) ((((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "le_n21")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 606    (BETA_TAC THEN (move ["le_n21"]));
 607    (((((use_arg_then "maxn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_n21")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((fun arg_tac -> (use_arg_then "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)));
 608    ((((use_arg_then "contra") (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "n1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac));
 609 ];;
 610
 611 (* Lemma leq_maxl *)
 612 let leq_maxl = section_proof ["m";"n1";"n2"] `(maxn n1 n2 <= m) <=> (n1 <= m) /\ (n2 <= m)` [
 613    (((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_maxr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 614 ];;
 615
 616 (* Lemma addn_maxl *)
 617 let addn_maxl = section_proof [] `!m1 m2 n. (maxn m1 m2) + n = maxn (m1 + n) (m2 + n)` [
 618    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((repeat_tactic 1 9 (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnAC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 619 ];;
 620
 621 (* Lemma addn_maxr *)
 622 let addn_maxr = section_proof [] `!m n1 n2. m + maxn n1 n2 = maxn (m + n1) (m + n2)` [
 623    ((BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"])) THEN ((repeat_tactic 1 9 (((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`m + _1`)]))))) THEN (((use_arg_then "addn_maxl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 624 ];;
 625
 626 (* Lemma min0n *)
 627 let min0n = section_proof ["n"] `minn 0 n = 0` [
 628    ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 629 ];;
 630
 631 (* Lemma minn0 *)
 632 let minn0 = section_proof ["n"] `minn n 0 = 0` [
 633    ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 634 ];;
 635
 636 (* Lemma minnC *)
 637 let minnC = section_proof ["m";"n"] `minn m n = minn n m` [
 638    ((repeat_tactic 1 9 (((use_arg_then "minn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
 639 ];;
 640
 641 (* Lemma minnr *)
 642 let minnr = section_proof ["m";"n"] `n <= m ==> minn m n = n` [
 643    ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 644 ];;
 645
 646 (* Lemma minnl *)
 647 let minnl = section_proof ["m";"n"] `m <= n ==> minn m n = m` [
 648    (((DISCH_THEN (fun snd_th -> (use_arg_then "minnr") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 649 ];;
 650
 651 (* Lemma addn_min_max *)
 652 let addn_min_max = section_proof ["m";"n"] `minn m n + maxn m n = m + n` [
 653    (((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
 654 ];;
 655
 656 (* Lemma minn_to_maxn *)
 657 let minn_to_maxn = section_proof ["m";"n"] `minn m n = (m + n) - maxn m n` [
 658    (((((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 659 ];;
 660
 661 (* Lemma sub_sub_minn *)
 662 let sub_sub_minn = section_proof ["m";"n"] `m - (m - n) = minn m n` [
 663    (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minn_to_maxn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add_sub_maxn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 664 ];;
 665
 666 (* Lemma minnCA *)
 667 let minnCA = section_proof [] `!m1 m2 m3. minn m1 (minn m2 m3) = minn m2 (minn m1 m3)` [
 668    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["m3"])) THEN (repeat_tactic 1 9 (((use_arg_then "minn_to_maxn")(thm_tac (new_rewrite [] [(`minn _1 (minn _2 _3)`)]))))));
 669    ((((fun arg_tac -> (use_arg_then "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_then "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_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))));
 670    (((repeat_tactic 1 9 (((use_arg_then "addn_maxl")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "addn_min_max")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "addn_maxr")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnAC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [(`m2 + m1`)]))))) THEN (done_tac));
 671 ];;
 672
 673 (* Lemma minnA *)
 674 let minnA = section_proof [] `!m1 m2 m3. minn m1 (minn m2 m3) = minn (minn m1 m2) m3` [
 675    (BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["m3"]));
 676    (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [(`minn m2 _1`)])))) THEN (((use_arg_then "minnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 677 ];;
 678
 679 (* Lemma minnAC *)
 680 let minnAC = section_proof ["m1";"m2";"m3"] `minn (minn m1 m2) m3 = minn (minn m1 m3) m2` [
 681    (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 682 ];;
 683
 684 (* Lemma eqn_minr *)
 685 let eqn_minr = section_proof ["m";"n"] `(minn m n = n) = (n <= m)` [
 686    (((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))));
 687    (((((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] [(`n + m`)]))))) THEN (((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`m = _1`)])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_maxl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 688 ];;
 689
 690 (* Lemma eqn_minl *)
 691 let eqn_minl = section_proof ["m";"n"] `(minn m n = m) = (m <= n)` [
 692    (((((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`_1 = m + n`)])))) THEN (((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_maxr")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 693 ];;
 694
 695 (* Lemma minnn *)
 696 let minnn = section_proof ["n"] `minn n n = n` [
 697    (((((use_arg_then "minnr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 698 ];;
 699
 700 (* Lemma leq_minr *)
 701 let leq_minr = section_proof ["m";"n1";"n2"] `(m <= minn n1 n2) <=> (m <= n1) /\ (m <= n2)` [
 702    ((((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 703 ];;
 704
 705 (* Lemma leq_minl *)
 706 let leq_minl = section_proof ["m";"n1";"n2"] `(minn n1 n2 <= m) <=> (n1 <= m) \/ (n2 <= m)` [
 707    (((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_minr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "negb_and")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 708 ];;
 709
 710 (* Lemma addn_minl *)
 711 let addn_minl = section_proof [] `!m1 m2 n. (minn m1 m2) + n = minn (m1 + n) (m2 + n)` [
 712    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((repeat_tactic 1 9 (((use_arg_then "minn_to_maxn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addn_maxl")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnAC")(thm_tac (new_rewrite [] []))))));
 713    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 + n`)])))))) THEN (((use_arg_then "addn_subA")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "addn_min_max")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 714 ];;
 715
 716 (* Lemma addn_minr *)
 717 let addn_minr = section_proof [] `!m n1 n2. m + minn n1 n2 = minn (m + n1) (m + n2)` [
 718    (BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"]));
 719    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "addnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`m + _1`)]))))) THEN (((use_arg_then "addn_minl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 720 ];;
 721
 722 (* Lemma maxnK *)
 723 let maxnK = section_proof ["m";"n"] `minn (maxn m n) m = m` [
 724    (((((use_arg_then "minnr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leq_maxr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 725 ];;
 726
 727 (* Lemma maxKn *)
 728 let maxKn = section_proof ["m";"n"] `minn n (maxn m n) = n` [
 729    (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 730 ];;
 731
 732 (* Lemma minnK *)
 733 let minnK = section_proof ["m";"n"] `maxn (minn m n) m = m` [
 734    (((((use_arg_then "maxnr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leq_minl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 735 ];;
 736
 737 (* Lemma minKn *)
 738 let minKn = section_proof ["m";"n"] `maxn n (minn m n) = n` [
 739    (((((use_arg_then "minnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "minnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 740 ];;
 741
 742 (* Lemma maxn_minl *)
 743 let maxn_minl = section_proof ["m1";"m2";"n"] `maxn (minn m1 m2) n = minn (maxn m1 n) (maxn m2 n)` [
 744    (((repeat_tactic 1 9 (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "minn")(thm_tac (new_rewrite [] [])))))) THEN (arith_tac));
 745 ];;
 746
 747 (* Lemma maxn_minr *)
 748 let maxn_minr = section_proof ["m";"n1";"n2"] `maxn m (minn n1 n2) = minn (maxn m n1) (maxn m n2)` [
 749    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "maxnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`maxn m _1`)]))))) THEN (((use_arg_then "maxn_minl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 750 ];;
 751
 752 (* Lemma minn_maxl *)
 753 let minn_maxl = section_proof [] `!m1 m2 n. minn (maxn m1 m2) n = maxn (minn m1 n) (minn m2 n)` [
 754    ((BETA_TAC THEN (move ["m1"]) THEN (move ["m2"]) THEN (move ["n"])) THEN ((((use_arg_then "maxn_minr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "maxn_minl")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "minnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "maxnC")(thm_tac (new_rewrite [] [(`maxn _1 n`)])))) THEN (repeat_tactic 1 9 (((use_arg_then "maxnK")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 755 ];;
 756
 757 (* Lemma minn_maxr *)
 758 let minn_maxr = section_proof [] `!m n1 n2. minn m (maxn n1 n2) = maxn (minn m n1) (minn m n2)` [
 759    (BETA_TAC THEN (move ["m"]) THEN (move ["n1"]) THEN (move ["n2"]));
 760    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "minnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`minn m _1`)]))))) THEN (((use_arg_then "minn_maxl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 761 ];;
 762
 763 (* Section Iteration *)
 764 begin_section "Iteration";;
 765 (add_section_var (mk_var ("m", (`:num`))); add_section_var (mk_var ("n", (`:num`))));;
 766 (add_section_var (mk_var ("x", (`:A`))); add_section_var (mk_var ("y", (`:A`))));;
 767 let iter = define `iter (SUC n) f (x:A) = f (iter n f x) /\ iter 0 f x = x`;;
 768 let iteri = define `iteri (SUC n) f (x:A) = f n (iteri n f x) /\ iteri 0 f x = x`;;
 769
 770 (* Lemma iterSr *)
 771 let iterSr = section_proof ["n";"f";"x"] `iter (SUC n) f (x : A) = iter n f (f x)` [
 772    ((((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) THEN ((repeat_tactic 1 9 (((use_arg_then "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));
 773 ];;
 774
 775 (* Lemma iterS *)
 776 let iterS = section_proof ["n";"f";"x"] `iter (SUC n) f (x:A) = f (iter n f x)` [
 777    ((((use_arg_then "iter")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
 778 ];;
 779
 780 (* Lemma iter_add *)
 781 let iter_add = section_proof ["n";"m";"f";"x"] `iter (n + m) f (x:A) = iter n f (iter m f x)` [
 782    ((((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) THEN (((repeat_tactic 1 9 (((use_arg_then "iter")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (((use_arg_then "add0n")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN ((TRY done_tac)) THEN (((use_arg_then "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_then "iterS")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 783 ];;
 784
 785 (* Lemma iteriS *)
 786 let iteriS = section_proof ["n";"f";"x"] `iteri (SUC n) f x = f n (iteri n f (x:A))` [
 787    ((((use_arg_then "iteri")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
 788 ];;
 789
 790 (* Finalization of the section Iteration *)
 791 let iterSr = finalize_theorem iterSr;;
 792 let iterS = finalize_theorem iterS;;
 793 let iter_add = finalize_theorem iter_add;;
 794 let iteriS = finalize_theorem iteriS;;
 795 end_section "Iteration";;
 796
 797 (* Lemma mul0n *)
 798 let mul0n = section_proof ["n"] `0 * n = 0` [
 799    ((arith_tac) THEN (done_tac));
 800 ];;
 801
 802 (* Lemma muln0 *)
 803 let muln0 = section_proof ["n"] `n * 0 = 0` [
 804    ((arith_tac) THEN (done_tac));
 805 ];;
 806
 807 (* Lemma mul1n *)
 808 let mul1n = section_proof ["n"] `1 * n = n` [
 809    ((arith_tac) THEN (done_tac));
 810 ];;
 811
 812 (* Lemma mulSn *)
 813 let mulSn = section_proof ["m";"n"] `SUC m * n = n + m * n` [
 814    (arith_tac);
 815 ];;
 816
 817 (* Lemma mulSnr *)
 818 let mulSnr = section_proof ["m";"n"] `SUC m * n = m * n + n` [
 819    (arith_tac);
 820 ];;
 821
 822 (* Lemma mulnS *)
 823 let mulnS = section_proof ["m";"n"] `m * SUC n = m + m * n` [
 824    ((((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) THEN (((repeat_tactic 0 10 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["m"])));
 825    ((((repeat_tactic 1 9 (((use_arg_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "addSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 826 ];;
 827
 828 (* Lemma mulnSr *)
 829 let mulnSr = section_proof ["m";"n"] `m * SUC n = m * n + m` [
 830    (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnS")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 831 ];;
 832
 833 (* Lemma muln1 *)
 834 let muln1 = section_proof ["n"] `n * 1 = n` [
 835    (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `1 = SUC 0`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnSr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 836 ];;
 837
 838 (* Lemma mulnC *)
 839 let mulnC = section_proof [] `!m n. m * n = n * m` [
 840    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
 841    (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; (move ["m"])]) THEN (((repeat_tactic 0 10 (((use_arg_then "muln0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mulnS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 842 ];;
 843
 844 (* Lemma muln_addl *)
 845 let muln_addl = section_proof ["m1";"m2";"n"] `(m1 + m2) * n = m1 * n + m2 * n` [
 846    ((THENL_FIRST) ((THENL) (((use_arg_then "m1") (disch_tac [])) THEN (clear_assumption "m1") THEN elim) [ALL_TAC; ((move ["m1"]) THEN (move ["IHm"]))]) (((((use_arg_then "mul0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "add0n")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
 847    (((((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHm")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mulSn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addSn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 848 ];;
 849
 850 (* Lemma muln_addr *)
 851 let muln_addr = section_proof ["m";"n1";"n2"] `m * (n1 + n2) = m * n1 + m * n2` [
 852    (((repeat_tactic 1 9 (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (((use_arg_then "muln_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 853 ];;
 854
 855 (* Lemma muln_subl *)
 856 let muln_subl = section_proof [] `!m n p. (m - n) * p = m * p - n * p` [
 857    ((THENL_FIRST) (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN ((THENL) case [ALL_TAC; (move ["n'"])])) (((repeat_tactic 1 9 (((use_arg_then "muln0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 858    ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "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_then "mul0n")(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then "sub0n")(fun tmp_arg1 -> (use_arg_then "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_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] []))))));
 859    (((((use_arg_then "IHm")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 860 ];;
 861
 862 (* Lemma muln_subr *)
 863 let muln_subr = section_proof [] `!m n p. m * (n - p) = m * n - m * p` [
 864    ((BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"])) THEN ((repeat_tactic 1 9 (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (((use_arg_then "muln_subl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 865 ];;
 866
 867 (* Lemma mulnA *)
 868 let mulnA = section_proof [] `!m n p. m * (n * p) = (m * n) * p` [
 869    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]) THEN (move ["p"]));
 870    ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; (move ["m"])]) ((repeat_tactic 1 9 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 871    ((((repeat_tactic 1 9 (((use_arg_then "mulSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln_addl")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 872 ];;
 873
 874 (* Lemma mulnCA *)
 875 let mulnCA = section_proof ["m";"n1";"n2"] `m * (n1 * n2) = n1 * (m * n2)` [
 876    (((repeat_tactic 1 9 (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (done_tac));
 877 ];;
 878
 879 (* Lemma mulnAC *)
 880 let mulnAC = section_proof ["m";"n";"p"] `(n * m) * p = (n * p) * m` [
 881    (((repeat_tactic 1 9 (((use_arg_then "mulnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`p * _1`)]))))) THEN (done_tac));
 882 ];;
 883
 884 (* Lemma muln_eq0 *)
 885 let muln_eq0 = section_proof ["m";"n"] `(m * n = 0) <=> (m = 0) \/ (n = 0)` [
 886    ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "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_then "muln0")(fun tmp_arg1 -> (use_arg_then "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));
 887 ];;
 888
 889 (* Lemma eqn_mul1 *)
 890 let eqn_mul1 = section_proof ["m";"n"] `(m * n = 1) <=> (m = 1) /\ (n = 1)` [
 891    ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "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));
 892 ];;
 893
 894 (* Lemma muln_gt0 *)
 895 let muln_gt0 = section_proof ["m";"n"] `(0 < m * n) <=> (0 < m) /\ (0 < n)` [
 896    ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "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));
 897 ];;
 898
 899 (* Lemma leq_pmull *)
 900 let leq_pmull = section_proof ["m";"n"] `0 < n ==> m <= n * m` [
 901    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addr")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 902 ];;
 903
 904 (* Lemma leq_pmulr *)
 905 let leq_pmulr = section_proof ["m";"n"] `0 < n ==> m <= m * n` [
 906    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then "leq_pmull") (fun fst_arg -> (use_arg_then "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_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 907 ];;
 908
 909 (* Lemma leq_mul2l *)
 910 let leq_mul2l = section_proof ["m";"n1";"n2"] `(m * n1 <= m * n2) <=> (m = 0) \/ (n1 <= n2)` [
 911    (((((use_arg_then "leqE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_subr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln_eq0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 912 ];;
 913
 914 (* Lemma leq_mul2r *)
 915 let leq_mul2r = section_proof ["m";"n1";"n2"] `(n1 * m <= n2 * m) <=> (m = 0) \/ (n1 <= n2)` [
 916    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * m`)])))))) THEN (((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 917 ];;
 918
 919 (* Lemma leq_mul *)
 920 let leq_mul = section_proof ["m1";"m2";"n1";"n2"] `m1 <= n1 ==> m2 <= n2 ==> m1 * m2 <= n1 * n2` [
 921    (BETA_TAC THEN (move ["le_mn1"]) THEN (move ["le_mn2"]));
 922    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "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);
 923    ((THENL_FIRST) (ANTS_TAC) (((((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_mn2")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 924    (DISCH_THEN apply_tac);
 925    (((((use_arg_then "leq_mul2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_mn1")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 926 ];;
 927
 928 (* Lemma eqn_mul2l *)
 929 let eqn_mul2l = section_proof ["m";"n1";"n2"] `(m * n1 = m * n2) <=> (m = 0) \/ (n1 = n2)` [
 930    (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "orb_andr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 931 ];;
 932
 933 (* Lemma eqn_mul2r *)
 934 let eqn_mul2r = section_proof ["m";"n1";"n2"] `(n1 * m = n2 * m) <=> (m = 0) \/ (n1 = n2)` [
 935    (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_mul2r")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "orb_andr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 936 ];;
 937
 938 (* Lemma leq_pmul2l *)
 939 let leq_pmul2l = section_proof ["m";"n1";"n2"] `0 < m ==> ((m * n1 <= m * n2) <=> (n1 <= n2))` [
 940    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
 941 ];;
 942
 943 (* Lemma leq_pmul2r *)
 944 let leq_pmul2r = section_proof ["m";"n1";"n2"] `0 < m ==> ((n1 * m <= n2 * m) <=> (n1 <= n2))` [
 945    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "leq_mul2r")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
 946 ];;
 947
 948 (* Lemma eqn_pmul2l *)
 949 let eqn_pmul2l = section_proof ["m";"n1";"n2"] `0 < m ==> ((m * n1 = m * n2) <=> (n1 = n2))` [
 950    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "eqn_mul2l")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
 951 ];;
 952
 953 (* Lemma eqn_pmul2r *)
 954 let eqn_pmul2r = section_proof ["m";"n1";"n2"] `0 < m ==> ((n1 * m = n2 * m) <=> (n1 = n2))` [
 955    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "eqn_mul2r")(thm_tac (new_rewrite [] [])))) THEN ((((use_arg_then "NOT_SUC")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "orFb")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
 956 ];;
 957
 958 (* Lemma ltn_mul2l *)
 959 let ltn_mul2l = section_proof ["m";"n1";"n2"] `(m * n1 < m * n2) <=> (0 < m) /\ (n1 < n2)` [
 960    (((((use_arg_then "lt0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 961 ];;
 962
 963 (* Lemma ltn_mul2r *)
 964 let ltn_mul2r = section_proof ["m";"n1";"n2"] `(n1 * m < n2 * m) <=> (0 < m) /\ (n1 < n2)` [
 965    (((((use_arg_then "lt0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_mul2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 966 ];;
 967
 968 (* Lemma ltn_pmul2l *)
 969 let ltn_pmul2l = section_proof ["m";"n1";"n2"] `0 < m ==> ((m * n1 < m * n2) <=> (n1 < n2))` [
 970    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "ltn_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 971 ];;
 972
 973 (* Lemma ltn_pmul2r *)
 974 let ltn_pmul2r = section_proof ["m";"n1";"n2"] `0 < m ==> (n1 * m < n2 * m <=> n1 < n2)` [
 975    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "ltn_mul2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 976 ];;
 977
 978 (* Lemma ltn_Pmull *)
 979 let ltn_Pmull = section_proof ["m";"n"] `1 < n ==> 0 < m ==> m < n * m` [
 980    ((BETA_TAC THEN (move ["lt1n"]) THEN (move ["m_gt0"])) THEN ((((use_arg_then "mul1n")(gsym_then (thm_tac (new_rewrite [1] [(`m`)]))))) THEN (((use_arg_then "ltn_pmul2r")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 981 ];;
 982
 983 (* Lemma ltn_Pmulr *)
 984 let ltn_Pmulr = section_proof ["m";"n"] `1 < n ==> 0 < m ==> m < m * n` [
 985    ((BETA_TAC THEN (move ["lt1n"]) THEN (move ["m_gt0"])) THEN ((((use_arg_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_Pmull")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 986 ];;
 987
 988 (* Lemma ltn_mul *)
 989 let ltn_mul = section_proof ["m1";"m2";"n1";"n2"] `m1 < n1 ==> m2 < n2 ==> m1 * m2 < n1 * n2` [
 990    (BETA_TAC THEN (move ["lt_mn1"]) THEN (move ["lt_mn2"]));
 991    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "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);
 992    (ANTS_TAC);
 993    (((((use_arg_then "leq_mul2l")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 994    (DISCH_THEN apply_tac);
 995    ((((use_arg_then "ltn_pmul2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 996    ((((use_arg_then "lt_mn2") (disch_tac [])) THEN (clear_assumption "lt_mn2") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 997 ];;
 998
 999 (* Lemma maxn_mulr *)
1000 let maxn_mulr = section_proof ["m";"n1";"n2"] `m * maxn n1 n2 = maxn (m * n1) (m * n2)` [
1001    ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["n"])]) (((repeat_tactic 1 9 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "maxnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1002    (((repeat_tactic 1 9 (((use_arg_then "maxn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "fun_if")(thm_tac (new_rewrite [] [(`SUC n * _1`)])))) THEN (((use_arg_then "ltn_pmul2l")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1003 ];;
1004
1005 (* Lemma maxn_mull *)
1006 let maxn_mull = section_proof ["m1";"m2";"n"] `maxn m1 m2 * n = maxn (m1 * n) (m2 * n)` [
1007    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * n`)])))))) THEN (((use_arg_then "maxn_mulr")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1008 ];;
1009
1010 (* Lemma minn_mulr *)
1011 let minn_mulr = section_proof ["m";"n1";"n2"] `m * minn n1 n2 = minn (m * n1) (m * n2)` [
1012    ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["n"])]) (((repeat_tactic 1 9 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "minn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "if_same")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1013    ((repeat_tactic 1 9 (((use_arg_then "minn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "fun_if")(thm_tac (new_rewrite [] [(`SUC n * _1`)])))) THEN (((use_arg_then "ltn_pmul2l")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "LT_0")(thm_tac (new_rewrite [] [])))));
1014 ];;
1015
1016 (* Lemma minn_mull *)
1017 let minn_mull = section_proof ["m1";"m2";"n"] `minn m1 m2 * n = minn (m1 * n) (m2 * n)` [
1018    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [(`_1 * n`)])))))) THEN (((use_arg_then "minn_mulr")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1019 ];;
1020 parse_as_infix("^", (24, "left"));;
1021 override_interface("^", `EXP`);;
1022
1023 (* Lemma expn0 *)
1024 let expn0 = section_proof ["m"] `m ^ 0 = 1` [
1025    ((((use_arg_then "EXP")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1026 ];;
1027
1028 (* Lemma expn1 *)
1029 let expn1 = section_proof ["m"] `m ^ 1 = m` [
1030    ((((use_arg_then "EXP_1")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1031 ];;
1032
1033 (* Lemma expnS *)
1034 let expnS = section_proof ["m";"n"] `m ^ SUC n = m * m ^ n` [
1035    ((((use_arg_then "EXP")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1036 ];;
1037
1038 (* Lemma expnSr *)
1039 let expnSr = section_proof ["m";"n"] `m ^ SUC n = m ^ n * m` [
1040    (((((use_arg_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1041 ];;
1042
1043 (* Lemma exp0n *)
1044 let exp0n = section_proof ["n"] `0 < n ==> 0 ^ n = 0` [
1045    ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) ((((use_arg_then "LT_REFL")(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
1046    (((((use_arg_then "EXP")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1047 ];;
1048
1049 (* Lemma exp1n *)
1050 let exp1n = section_proof ["n"] `1 ^ n = 1` [
1051    (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [(((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))); ((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul1n")(thm_tac (new_rewrite [] [])))))]) THEN (done_tac));
1052 ];;
1053
1054 (* Lemma expn_add *)
1055 let expn_add = section_proof ["m";"n1";"n2"] `m ^ (n1 + n2) = m ^ n1 * m ^ n2` [
1056    (((THENL) (((use_arg_then "n1") (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) THEN ((repeat_tactic 0 10 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mul1n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "addSn")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))))));
1057    (((((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1058 ];;
1059
1060 (* Lemma expn_mull *)
1061 let expn_mull = section_proof ["m1";"m2";"n"] `(m1 * m2) ^ n = m1 ^ n * m2 ^ n` [
1062    ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((repeat_tactic 1 9 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln1")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1063    (((repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "mulnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnCA")(thm_tac (new_rewrite [] [(`m2 * _1`)]))))) THEN (done_tac));
1064 ];;
1065
1066 (* Lemma expn_mulr *)
1067 let expn_mulr = section_proof ["m";"n1";"n2"] `m ^ (n1 * n2) = (m ^ n1) ^ n2` [
1068    ((THENL_FIRST) ((THENL) (((use_arg_then "n1") (disch_tac [])) THEN (clear_assumption "n1") THEN elim) [ALL_TAC; ((move ["n1"]) THEN (move ["IHn"]))]) (((repeat_tactic 1 9 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mul0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "exp1n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1069    (((((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn_mull")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1070 ];;
1071
1072 (* Lemma expn_gt0 *)
1073 let expn_gt0 = section_proof ["m";"n"] `(0 < m ^ n) <=> (0 < m) \/ (n = 0)` [
1074    ((THENL_FIRST) (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; (move ["m"])]) THEN ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))])) ((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
1075    (((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
1076    ((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
1077    (((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
1078 ];;
1079
1080 (* Lemma expn_eq0 *)
1081 let expn_eq0 = section_proof ["m";"e"] `(m ^ e = 0) <=> (m = 0) /\ (0 < e)` [
1082    (((repeat_tactic 1 9 (((use_arg_then "eqn0Ngt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "lt0n")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1083 ];;
1084
1085 (* Lemma ltn_expl *)
1086 let ltn_expl = section_proof ["m";"n"] `1 < m ==> n < m ^ n` [
1087    ((THENL_FIRST) ((BETA_TAC THEN (move ["m_gt1"])) THEN ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])])) ((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
1088    ((((fun arg_tac -> (use_arg_then "ltnW") (fun fst_arg -> (use_arg_then "m_gt1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "leq_pmul2l") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC));
1089    (((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
1090    ((((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] []))))));
1091    ((((fun arg_tac -> (use_arg_then "ltn_Pmull") (fun fst_arg -> (use_arg_then "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));
1092 ];;
1093
1094 (* Lemma leq_exp2l *)
1095 let leq_exp2l = section_proof ["m";"n1";"n2"] `1 < m ==> (m ^ n1 <= m ^ n2 <=> n1 <= n2)` [
1096    ((THENL_ROT (-1)) ((BETA_TAC THEN (move ["m_gt1"])) THEN ((THENL) (((use_arg_then "n2") (disch_tac [])) THEN (clear_assumption "n2") THEN ((use_arg_then "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_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))));
1097    (((repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_pmul2l")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "leqSS")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1098    (((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expn_gt0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "m_gt1") (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
1099    ((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))));
1100    ((((use_arg_then "m_gt1") (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN ((((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (move ["m_gt1"])));
1101    ((((use_arg_then "ltE")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "leq_trans") (fun fst_arg -> (use_arg_then "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_then "ltE")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then "ltn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_pmulr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "expn_gt0")(thm_tac (new_rewrite [] [])))));
1102    ((((use_arg_then "m_gt1") (disch_tac [])) THEN (clear_assumption "m_gt1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
1103 ];;
1104
1105 (* Lemma ltn_exp2l *)
1106 let ltn_exp2l = section_proof ["m";"n1";"n2"] `1 < m ==> (m ^ n1 < m ^ n2 <=> n1 < n2)` [
1107    ((BETA_TAC THEN (move ["m_gt1"])) THEN ((repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_exp2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1108 ];;
1109
1110 (* Lemma eqn_exp2l *)
1111 let eqn_exp2l = section_proof ["m";"n1";"n2"] `1 < m ==> (m ^ n1 = m ^ n2 <=> n1 = n2)` [
1112    ((BETA_TAC THEN (move ["m_gt1"])) THEN ((repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_exp2l")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1113 ];;
1114
1115 (* Lemma expnI *)
1116 let expnI = section_proof ["m"] `1 < m ==> !e1 e2. m ^ e1 = m ^ e2 ==> e1 = e2` [
1117    ((BETA_TAC THEN (move ["m_gt1"]) THEN (move ["e1"]) THEN (move ["e2"])) THEN (((use_arg_then "eqn_exp2l")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1118 ];;
1119
1120 (* Lemma leq_pexp2l *)
1121 let leq_pexp2l = section_proof ["m";"n1";"n2"] `0 < m ==> n1 <= n2 ==> m ^ n1 <= m ^ n2` [
1122    (((THENL) (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((repeat_tactic 0 10 (((use_arg_then "ltn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))) [((((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "exp1n")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))); ((((use_arg_then "leq_exp2l")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))]) THEN (arith_tac) THEN (done_tac));
1123 ];;
1124
1125 (* Lemma ltn_pexp2l *)
1126 let ltn_pexp2l = section_proof ["m";"n1";"n2"] `0 < m ==> m ^ n1 < m ^ n2 ==> n1 < n2` [
1127    (((THENL) (((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN case) [ALL_TAC; ((THENL) case [ALL_TAC; (move ["m"])])]) THEN ((repeat_tactic 0 10 (((use_arg_then "ltn0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)))) [((((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "exp1n")(thm_tac (new_rewrite [] [])))))); (((use_arg_then "ltn_exp2l")(thm_tac (new_rewrite [] []))))]) THEN (arith_tac) THEN (done_tac));
1128 ];;
1129
1130 (* Lemma ltn_exp2r *)
1131 let ltn_exp2r = section_proof ["m";"n";"e"] `0 < e ==> (m ^ e < n ^ e <=> m < n)` [
1132    ((BETA_TAC THEN (move ["e_gt0"])) THEN ((THENL) (split_tac) [ALL_TAC; (move ["ltmn"])]));
1133    ((repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "contra") (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (move ["lemn"])));
1134    (((THENL) (((use_arg_then "e") (disch_tac [])) THEN (clear_assumption "e") THEN elim) [ALL_TAC; ((move ["e'"]) THEN (move ["IHe"]))]) THEN ((repeat_tactic 0 10 (((use_arg_then "expn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_mul")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1135    ((THENL_FIRST) (((use_arg_then "e_gt0") (disch_tac [])) THEN (clear_assumption "e_gt0") THEN ((use_arg_then "e") (disch_tac [])) THEN (clear_assumption "e") THEN elim) ((((use_arg_then "ltnn")(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
1136    ((THENL_FIRST) (BETA_TAC THEN ((THENL) case [ALL_TAC; ((move ["e"]) THEN (move ["IHe"]))])) (((((use_arg_then "ONE")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "expn1")(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
1137    (((repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "ltn_mul")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "IHe")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac));
1138 ];;
1139
1140 (* Lemma leq_exp2r *)
1141 let leq_exp2r = section_proof ["m";"n";"e"] `0 < e ==> (m ^ e <= n ^ e <=> m <= n)` [
1142    ((BETA_TAC THEN (move ["e_gt0"])) THEN ((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1143 ];;
1144
1145 (* Lemma eqn_exp2r *)
1146 let eqn_exp2r = section_proof ["m";"n";"e"] `0 < e ==> (m ^ e = n ^ e <=> m = n)` [
1147    ((BETA_TAC THEN (move ["e_gt0"])) THEN ((repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "leq_exp2r")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1148 ];;
1149
1150 (* Lemma expIn *)
1151 let expIn = section_proof ["e"] `0 < e ==> !m n. m ^ e = n ^ e ==> m = n` [
1152    ((BETA_TAC THEN (move ["e_gt0"]) THEN (move ["m"]) THEN (move ["n"])) THEN (((use_arg_then "eqn_exp2r")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1153 ];;
1154
1155 (* Lemma fact0 *)
1156 let fact0 = section_proof [] `FACT 0 = 1` [
1157    ((((use_arg_then "FACT")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1158 ];;
1159
1160 (* Lemma factS *)
1161 let factS = section_proof ["n"] `FACT (SUC n)  = (SUC n) * FACT n` [
1162    ((((use_arg_then "FACT")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1163 ];;
1164
1165 (* Lemma fact_gt0 *)
1166 let fact_gt0 = section_proof ["n"] `0 < FACT n` [
1167    (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])]) THEN ((((use_arg_then "FACT")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (repeat_tactic 0 10 (((use_arg_then "muln_gt0")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))))) THEN (arith_tac) THEN (done_tac));
1168 ];;
1169 let odd = new_basic_definition `odd = ODD`;;
1170
1171 (* Lemma odd0 *)
1172 let odd0 = section_proof [] `odd 0 = F` [
1173    ((((use_arg_then "odd")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 2 0 (((use_arg_then "ODD")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1174 ];;
1175
1176 (* Lemma oddS *)
1177 let oddS = section_proof ["n"] `odd (SUC n) = ~odd n` [
1178    (((((use_arg_then "odd")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "ODD")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1179 ];;
1180
1181 (* Lemma odd1 *)
1182 let odd1 = section_proof [] `odd 1 = T` [
1183    (((((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1184 ];;
1185
1186 (* Lemma odd_add *)
1187 let odd_add = section_proof ["m";"n"] `odd (m + n) = odd m + odd n` [
1188    ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHn"]))]) (((((use_arg_then "add0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addFb")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1189    (((((use_arg_then "addSn")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "oddS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addTb")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addbA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addTb")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1190 ];;
1191
1192 (* Lemma odd_sub *)
1193 let odd_sub = section_proof ["m";"n"] `n <= m ==> odd (m - n) = odd m + odd n` [
1194    ((BETA_TAC THEN (move ["le_nm"])) THEN (((fun arg_tac -> (use_arg_then "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_then "odd_add")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subnK")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "addbK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1195 ];;
1196
1197 (* Lemma odd_opp *)
1198 let odd_opp = section_proof ["i";"m"] `odd m = F ==> i < m ==> odd (m - i) = odd i` [
1199    (BETA_TAC THEN (move ["oddm"]) THEN (move ["lt_im"]));
1200    (((((fun arg_tac -> (use_arg_then "odd_sub") (fun fst_arg -> (fun arg_tac -> (use_arg_then "ltnW") (fun fst_arg -> (use_arg_then "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_then "oddm")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addFb")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1201 ];;
1202
1203 (* Lemma odd_mul *)
1204 let odd_mul = section_proof ["m";"n"] `odd (m * n) <=> odd m /\ odd n` [
1205    ((THENL_FIRST) ((THENL) (((use_arg_then "m") (disch_tac [])) THEN (clear_assumption "m") THEN elim) [ALL_TAC; ((move ["m"]) THEN (move ["IHm"]))]) (((((use_arg_then "mul0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andFb")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1206    (((((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addTb")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "andb_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHm")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1207 ];;
1208
1209 (* Lemma odd_exp *)
1210 let odd_exp = section_proof ["m";"n"] `odd (m ^ n) <=> (n = 0) \/ odd m` [
1211    ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd1")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1212    ((((use_arg_then "expnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd_mul")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "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_then "orFb")(thm_tac (new_rewrite [] [])))));
1213    ((fun arg_tac -> arg_tac (Arg_term (`odd m`))) (term_tac (set_tac "b")));
1214    (((use_arg_then "IHn") (disch_tac [])) THEN (clear_assumption "IHn") THEN ((use_arg_then "b_def") (disch_tac [])) THEN (clear_assumption "b_def") THEN BETA_TAC THEN (move ["_"]) THEN (move ["_"]));
1215    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
1216 ];;
1217 let double = define `double 0 = 0 /\ (!n. double (SUC n) = SUC (SUC (double n)))`;;
1218
1219 (* Lemma double0 *)
1220 let double0 = section_proof [] `double 0 = 0` [
1221    ((((use_arg_then "double")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1222 ];;
1223
1224 (* Lemma doubleS *)
1225 let doubleS = section_proof ["n"] `double (SUC n) = SUC (SUC (double n))` [
1226    ((((use_arg_then "double")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (done_tac));
1227 ];;
1228
1229 (* Lemma addnn *)
1230 let addnn = section_proof ["n"] `n + n = double n` [
1231    ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "addn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1232    (((((use_arg_then "addnS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1233 ];;
1234
1235 (* Lemma mul2n *)
1236 let mul2n = section_proof ["m"] `2 * m = double m` [
1237    (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `2 = SUC 1`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulSn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul1n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1238 ];;
1239
1240 (* Lemma muln2 *)
1241 let muln2 = section_proof ["m"] `m * 2 = double m` [
1242    (((((use_arg_then "mulnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1243 ];;
1244
1245 (* Lemma double_add *)
1246 let double_add = section_proof ["m";"n"] `double (m + n) = double m + double n` [
1247    (((repeat_tactic 1 9 (((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then "addnCA") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [(`n + _1`)]))))) THEN (done_tac));
1248 ];;
1249
1250 (* Lemma double_sub *)
1251 let double_sub = section_proof ["m";"n"] `double (m - n) = double m - double n` [
1252    ((((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then "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_then "sub0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "sub0n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
1253    (((repeat_tactic 1 9 (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subSS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "IHm")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1254 ];;
1255
1256 (* Lemma leq_double *)
1257 let leq_double = section_proof ["m";"n"] `(double m <= double n <=> m <= n)` [
1258    (((repeat_tactic 1 9 (((use_arg_then "leqE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "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_then "double")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
1259 ];;
1260
1261 (* Lemma ltn_double *)
1262 let ltn_double = section_proof ["m";"n"] `(double m < double n) = (m < n)` [
1263    (((repeat_tactic 2 0 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_double")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1264 ];;
1265
1266 (* Lemma ltn_Sdouble *)
1267 let ltn_Sdouble = section_proof ["m";"n"] `(SUC (double m) < double n) = (m < n)` [
1268    ((repeat_tactic 1 9 (((use_arg_then "muln2")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
1269 ];;
1270
1271 (* Lemma leq_Sdouble *)
1272 let leq_Sdouble = section_proof ["m";"n"] `(double m <= SUC (double n)) = (m <= n)` [
1273    (((((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_Sdouble")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqNgt")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1274 ];;
1275
1276 (* Lemma odd_double *)
1277 let odd_double = section_proof ["n"] `odd (double n) = F` [
1278    (((((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "odd_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addbb")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1279 ];;
1280
1281 (* Lemma double_gt0 *)
1282 let double_gt0 = section_proof ["n"] `(0 < double n) = (0 < n)` [
1283    (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) THEN ((repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (arith_tac));
1284 ];;
1285
1286 (* Lemma double_eq0 *)
1287 let double_eq0 = section_proof ["n"] `(double n = 0) = (n = 0)` [
1288    (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["n"])]) THEN ((repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] []))))) THEN (arith_tac));
1289 ];;
1290
1291 (* Lemma double_mull *)
1292 let double_mull = section_proof ["m";"n"] `double (m * n) = double m * n` [
1293    (((repeat_tactic 1 9 (((use_arg_then "mul2n")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1294 ];;
1295
1296 (* Lemma double_mulr *)
1297 let double_mulr = section_proof ["m";"n"] `double (m * n) = m * double n` [
1298    (((repeat_tactic 1 9 (((use_arg_then "muln2")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mulnA")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1299 ];;
1300 let half_def = define `HALF 0 = (0, 0) /\
1301         !n. HALF (SUC n) = (SND (HALF n), SUC (FST (HALF n)))`;;
1302 let half = new_basic_definition `half = FST o HALF`;;
1303 let uphalf = new_basic_definition `uphalf = SND o HALF`;;
1304
1305 (* Lemma half0 *)
1306 let half0 = section_proof [] `half 0 = 0` [
1307    (((((use_arg_then "half")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1308 ];;
1309
1310 (* Lemma uphalf0 *)
1311 let uphalf0 = section_proof [] `uphalf 0 = 0` [
1312    (((((use_arg_then "uphalf")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1313 ];;
1314
1315 (* Lemma halfS *)
1316 let halfS = section_proof ["n"] `half (SUC n) = uphalf n` [
1317    (((((use_arg_then "half")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "uphalf")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1318 ];;
1319
1320 (* Lemma uphalfS *)
1321 let uphalfS = section_proof ["n"] `uphalf (SUC n) = SUC (half n)` [
1322    (((((use_arg_then "half")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "uphalf")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then "o_DEF")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac) THEN (((use_arg_then "half_def")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg])))) THEN (done_tac));
1323 ];;
1324
1325 (* Lemma doubleK *)
1326 let doubleK = section_proof ["x"] `half (double x) = x` [
1327    ((THENL_FIRST) ((THENL) (((use_arg_then "x") (disch_tac [])) THEN (clear_assumption "x") THEN elim) [ALL_TAC; (move ["n"])]) (((((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "half0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1328    ((((((use_arg_then "doubleS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "halfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1329 ];;
1330 let half_double = doubleK;;
1331
1332 (* Lemma double_inj *)
1333 let double_inj = section_proof [] `!m n. double m = double n ==> m = n` [
1334    (BETA_TAC THEN (move ["m"]) THEN (move ["n"]));
1335    ((((((use_arg_then "doubleK")(gsym_then (thm_tac (new_rewrite [2] [(`m`)]))))) THEN (((use_arg_then "doubleK")(gsym_then (thm_tac (new_rewrite [2] [(`n`)])))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1336 ];;
1337
1338 (* Lemma uphalf_double *)
1339 let uphalf_double = section_proof ["n"] `uphalf (double n) = n` [
1340    ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; (move ["n"])]) (((((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalf0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1341    ((((((use_arg_then "doubleS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1342 ];;
1343
1344 (* Lemma uphalf_half *)
1345 let uphalf_half = section_proof ["n"] `uphalf n = (if odd n then 1 else 0) + half n` [
1346    ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "uphalf0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "half0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1347    ((((use_arg_then "halfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "IHn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] [])))));
1348    ((((fun arg_tac -> arg_tac (Arg_term (`odd n`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((fun arg_tac ->(use_arg_then "add0n")(fun tmp_arg1 -> (use_arg_then "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_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1349 ];;
1350
1351 (* Lemma odd_double_half *)
1352 let odd_double_half = section_proof ["n"] `(if odd n then 1 else 0) + double (half n) = n` [
1353    ((THENL_FIRST) ((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["IHn"]))]) (((((use_arg_then "odd0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "half0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1354    ((((use_arg_then "IHn")(gsym_then (thm_tac (new_rewrite [3] []))))) THEN (((use_arg_then "halfS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "uphalf_half")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "double_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "oddS")(thm_tac (new_rewrite [] [])))));
1355    (((use_arg_then "IHn") (disch_tac [])) THEN (clear_assumption "IHn") THEN BETA_TAC THEN (move ["_"]));
1356    ((((fun arg_tac -> arg_tac (Arg_term (`odd n`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((repeat_tactic 0 10 (((use_arg_then "double0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "ONE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "doubleS")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "addSn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "double0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1357 ];;
1358
1359 (* Lemma half_bit_double *)
1360 let half_bit_double = section_proof ["n";"b"] `half ((if b then 1 else 0) + double n) = n` [
1361    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN ((simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac ->(use_arg_then "half_double")(fun tmp_arg1 -> (use_arg_then "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));
1362 ];;
1363
1364 (* Lemma half_add *)
1365 let half_add = section_proof ["m";"n"] `half (m + n) = (if odd m /\ odd n then 1 else 0) + (half m + half n)` [
1366    ((((use_arg_then "odd_double_half")(gsym_then (thm_tac (new_rewrite [1] [(`n`)]))))) THEN (((use_arg_then "addnCA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "odd_double_half")(gsym_then (thm_tac (new_rewrite [1] [(`m`)]))))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "double_add")(gsym_then (thm_tac (new_rewrite [] []))))));
1367    ((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_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "half_double")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalf_double")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
1368    ((((use_arg_then "half_double")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1369 ];;
1370
1371 (* Lemma half_leq *)
1372 let half_leq = section_proof ["m";"n"] `m <= n ==> half m <= half n` [
1373    (((DISCH_THEN (fun snd_th -> (use_arg_then "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_then "half_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leq_addl")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1374 ];;
1375
1376 (* Lemma half_gt0 *)
1377 let half_gt0 = section_proof ["n"] `(0 < half n) = (1 < n)` [
1378    (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (case THEN ALL_TAC)]) THEN ((repeat_tactic 0 10 (((use_arg_then "halfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalfS")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "uphalf0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "half0")(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
1379 ];;
1380
1381 (* Lemma mulnn *)
1382 let mulnn = section_proof ["m"] `m * m = m ^ 2` [
1383    (((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `2 = SUC (SUC 0)`)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "expnS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "expn0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln1")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1384 ];;
1385
1386 (* Lemma sqrn_add *)
1387 let sqrn_add = section_proof ["m";"n"] `(m + n) ^ 2 = (m ^ 2 + n ^ 2) + 2 * (m * n)` [
1388    ((repeat_tactic 1 9 (((use_arg_then "mulnn")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_addr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "muln_addl")(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))));
1389    (((((use_arg_then "EQ_ADD_LCANCEL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1390 ];;
1391
1392 (* Lemma sqrn_sub *)
1393 let sqrn_sub = section_proof ["m";"n"] `n <= m ==> (m - n) ^ 2 = (m ^ 2 + n ^ 2) - 2 * (m * n)` [
1394    ((DISCH_THEN (fun snd_th -> (use_arg_then "subnK") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["def_m"]));
1395    ((((use_arg_then "def_m")(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then "sqrn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnAC")(thm_tac (new_rewrite [] [])))));
1396    (((repeat_tactic 2 0 (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul2n")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "muln_addr")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mulnn")(gsym_then (thm_tac (new_rewrite [] [(`n EXP 2`)]))))) THEN (((use_arg_then "muln_addl")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "def_m")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1397 ];;
1398
1399 (* Lemma sqrn_add_sub *)
1400 let sqrn_add_sub = section_proof ["m";"n"] `n <= m ==> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2` [
1401    ((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_then "mulnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subn_sub")(gsym_then (thm_tac (new_rewrite [] [])))))));
1402    (((((use_arg_then "sqrn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnK")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "sqrn_sub")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1403 ];;
1404
1405 (* Lemma subn_sqr *)
1406 let subn_sqr = section_proof ["m";"n"] `m ^ 2 - n ^ 2 = (m - n) * (m + n)` [
1407    (((((use_arg_then "muln_subl")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "muln_addr")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "mulnC") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "mulnn")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1408 ];;
1409
1410 (* Lemma ltn_sqr *)
1411 let ltn_sqr = section_proof ["m";"n"] `(m ^ 2 < n ^ 2) = (m < n)` [
1412    (((((use_arg_then "ltn_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
1413 ];;
1414
1415 (* Lemma leq_sqr *)
1416 let leq_sqr = section_proof ["m";"n"] `(m ^ 2 <= n ^ 2) = (m <= n)` [
1417    (((((use_arg_then "leq_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
1418 ];;
1419
1420 (* Lemma sqrn_gt0 *)
1421 let sqrn_gt0 = section_proof ["n"] `(0 < n ^ 2) = (0 < n)` [
1422    ((THENL_FIRST) ((((fun arg_tac -> (use_arg_then "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_then "exp0n")(thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac)));
1423    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1424 ];;
1425
1426 (* Lemma eqn_sqr *)
1427 let eqn_sqr = section_proof ["m";"n"] `(m ^ 2 = n ^ 2) = (m = n)` [
1428    (((((use_arg_then "eqn_exp2r")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
1429 ];;
1430
1431 (* Lemma sqrn_inj *)
1432 let sqrn_inj = section_proof ["m";"n"] `m ^ 2 = n ^ 2 ==> m = n` [
1433    (BETA_TAC THEN (move ["eq"]));
1434    (((fun arg_tac -> (use_arg_then "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"]));
1435    ((((fun arg_tac -> (use_arg_then "inj") (fun fst_arg -> (use_arg_then "eq") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1436 ];;
1437 let leqif = new_definition `!m n c. leqif m n c <=> (m <= n /\ ((m = n) <=> c))`;;
1438
1439 (* Lemma leqifP *)
1440 let leqifP = section_proof ["m";"n";"c"] `leqif m n c <=> if c then m = n else m < n` [
1441    ((THENL_FIRST) (((((use_arg_then "ltn_neqAle")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqif")(thm_tac (new_rewrite [] []))))) THEN (split_tac)) ((((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac)));
1442    ((((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1443 ];;
1444
1445 (* Lemma leqif_imp_le *)
1446 let leqif_imp_le = section_proof ["m";"n";"c"] `leqif m n c ==> m <= n` [
1447    (((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
1448 ];;
1449
1450 (* Lemma leqif_imp_eq *)
1451 let leqif_imp_eq = section_proof ["m";"n";"c"] `leqif m n c ==> (m = n <=> c)` [
1452    (((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
1453 ];;
1454
1455 (* Lemma leqif_refl *)
1456 let leqif_refl = section_proof ["m";"c"] `(leqif m m c) <=> c` [
1457    (((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1458 ];;
1459
1460 (* Lemma leqif_trans *)
1461 let leqif_trans = section_proof ["m1";"m2";"m3";"c1";"c2"] `leqif m1 m2 c1 ==> leqif m2 m3 c2 ==> leqif m1 m3 (c1 /\ c2)` [
1462    (repeat_tactic 1 9 (((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))));
1463    ((THENL_FIRST) ((((use_arg_then "c1") (disch_tac [])) THEN (clear_assumption "c1") THEN case) THEN (((use_arg_then "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)));
1464    ((repeat_tactic 1 9 (((use_arg_then "ltE")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "leq_trans") (disch_tac [])) THEN (clear_assumption "leq_trans") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then "leqSS")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnW") (disch_tac [])) THEN (clear_assumption "ltnW") THEN (exact_tac)) THEN (done_tac));
1465 ];;
1466
1467 (* Lemma monotone_leqif *)
1468 let monotone_leqif = section_proof ["f"] `(!m n. f m <= f n <=> m <= n) ==>
1469   !m n c. (leqif (f m) (f n) c) <=> (leqif m n c)` [
1470    (BETA_TAC THEN (move ["f_mono"]) THEN (move ["m"]) THEN (move ["n"]) THEN (move ["c"]));
1471    (((repeat_tactic 1 9 (((use_arg_then "leqifP")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "f_mono")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1472 ];;
1473
1474 (* Lemma leqif_geq *)
1475 let leqif_geq = section_proof ["m";"n"] `m <= n ==> leqif m n (n <= m)` [
1476    ((BETA_TAC THEN (move ["lemn"])) THEN (((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN ((TRY done_tac))) THEN (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))));
1477    ((((use_arg_then "lemn")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1478 ];;
1479
1480 (* Lemma leqif_eq *)
1481 let leqif_eq = section_proof ["m";"n"] `m <= n ==> leqif m n (m = n)` [
1482    ((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1483 ];;
1484
1485 (* Lemma geq_leqif *)
1486 let geq_leqif = section_proof ["a";"b";"C"] `leqif a b C ==> ((b <= a) <=> C)` [
1487    ((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN (case THEN (move ["le_ab"])) THEN (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))));
1488    ((((use_arg_then "le_ab")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1489 ];;
1490
1491 (* Lemma ltn_leqif *)
1492 let ltn_leqif = section_proof ["a";"b";"C"] `leqif a b C ==> (a < b <=> ~ C)` [
1493    (BETA_TAC THEN (move ["le_ab"]));
1494    (((((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "geq_leqif") (fun fst_arg -> (use_arg_then "le_ab") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1495 ];;
1496
1497 (* Lemma leqif_add *)
1498 let leqif_add = section_proof ["m1";"n1";"c1";"m2";"n2";"c2"] `leqif m1 n1 c1 ==> leqif m2 n2 c2 ==> leqif (m1 + m2) (n1 + n2) (c1 /\ c2)` [
1499    ((((fun arg_tac -> (use_arg_then "monotone_leqif") (fun fst_arg -> (fun arg_tac -> (use_arg_then "leq_add2r") (fun fst_arg -> (use_arg_then "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"]));
1500    (((fun arg_tac -> (use_arg_then "monotone_leqif") (fun fst_arg -> (fun arg_tac -> (use_arg_then "leq_add2l") (fun fst_arg -> (use_arg_then "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 [] [])))));
1501    (((use_arg_then "leqif_trans") (disch_tac [])) THEN (clear_assumption "leqif_trans") THEN (exact_tac));
1502 ];;
1503
1504 (* Lemma leqif_mul *)
1505 let leqif_mul = section_proof ["m1";"n1";"c1";"m2";"n2";"c2"] `leqif m1 n1 c1 ==> leqif m2 n2 c2 ==>
1506           leqif (m1 * m2) (n1 * n2) (n1 * n2 = 0 \/ (c1 /\ c2))` [
1507    (BETA_TAC THEN (move ["le1"]) THEN (move ["le2"]));
1508    ((THENL) (((fun arg_tac -> (use_arg_then "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]);
1509    ((((use_arg_then "n12_0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le2") (disch_tac [])) THEN (clear_assumption "le2") THEN ((use_arg_then "le1") (disch_tac [])) THEN (clear_assumption "le1") THEN ((use_arg_then "n12_0") (disch_tac [])) THEN (clear_assumption "n12_0") THEN BETA_TAC) THEN (((use_arg_then "muln_eq0")(thm_tac (new_rewrite [] [])))));
1510    ((case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((THENL) (((use_arg_then "m2") (disch_tac [])) THEN (clear_assumption "m2") THEN ((use_arg_then "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_then "leqif")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "muln0")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "mul0n")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "leqnn")(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (arith_tac));
1511    ((((use_arg_then "muln_gt0")(thm_tac (new_rewrite [] [])))) THEN (BETA_TAC THEN (case THEN ((move ["n1_gt0"]) THEN (move ["n2_gt0"])))));
1512    (((fun arg_tac -> (use_arg_then "posnP") (fun fst_arg -> (use_arg_then "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"])]));
1513    ((((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le2") (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then "leqif")(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["_"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))))));
1514    (((((use_arg_then "andbC")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "m2_0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n1_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n2_gt0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1515    ((((use_arg_then "n1_gt0") (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then "leq_pmul2l") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "monotone_leqif") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["Mn1"])));
1516    (((use_arg_then "le2") (disch_tac [])) THEN (clear_assumption "le2") THEN ((use_arg_then "Mn1") (disch_tac [])) THEN (clear_assumption "Mn1") THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
1517    ((((use_arg_then "m2_gt0") (disch_tac [])) THEN (clear_assumption "m2_gt0") THEN (DISCH_THEN (fun snd_th -> (use_arg_then "leq_pmul2r") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then "monotone_leqif") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["Mm2"])));
1518    (((use_arg_then "le1") (disch_tac [])) THEN (clear_assumption "le1") THEN ((use_arg_then "Mm2") (disch_tac [])) THEN (clear_assumption "Mm2") THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
1519    (BETA_TAC THEN (move ["leq1"]) THEN (move ["leq2"]));
1520    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "leqif_trans") (fun fst_arg -> (use_arg_then "leq1") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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_then "leqifP")(thm_tac (new_rewrite [] []))))));
1521    (((fun arg_tac -> arg_tac (Arg_term (`c1 /\ c2`))) (disch_tac [])) THEN case THEN (simp_tac));
1522    (((((use_arg_then "eqn_leq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "muln_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n1_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "n2_gt0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1523 ];;
1524
1525 (* Lemma nat_Cauchy *)
1526 let nat_Cauchy = section_proof ["m";"n"] `leqif (2 * (m * n)) (m ^ 2 + n ^ 2) (m = n)` [
1527    ((fun arg_tac -> arg_tac (Arg_term (`n <= m`))) (term_tac (wlog_tac (move ["le_nm"])[`m`; `n`])));
1528    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "leqP") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN ((TRY done_tac))) THEN (((((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnC")(thm_tac (new_rewrite [] [(`m * _1`)]))))) THEN (move ["mn"])));
1529    ((((use_arg_then "le_nm") (disch_tac [])) THEN (clear_assumption "le_nm") THEN (DISCH_THEN apply_tac)) THEN (((fun arg_tac -> (use_arg_then "ltnW") (fun fst_arg -> (use_arg_then "mn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
1530    (BETA_TAC THEN (move ["le_nm"]));
1531    (((use_arg_then "leqifP")(thm_tac (new_rewrite [] []))));
1532    ((THENL_FIRST) ((THENL) (((fun arg_tac -> (use_arg_then "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_then "mulnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1533    (((((use_arg_then "ne_mn")(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (simp_tac)) THEN ((((use_arg_then "subn_gt0")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "sqrn_sub")(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "sqrn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subn_gt0")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_neqAle")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eq_sym")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1534 ];;
1535
1536 (* Lemma nat_AGM2 *)
1537 let nat_AGM2 = section_proof ["m";"n"] `leqif (4 * (m * n)) ((m + n) ^ 2) (m = n)` [
1538    ((((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `4 = 2 * 2`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "mulnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "mul2n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addnn")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "sqrn_add")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))));
1539    ((((use_arg_then "ltn_add2r")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "eqn_addr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltn_neqAle")(thm_tac (new_rewrite [] [])))));
1540    (((((fun arg_tac -> (use_arg_then "leqif_imp_eq") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "nat_Cauchy") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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_then "leqif_imp_le") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "nat_Cauchy") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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_then "if_same")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1541 ];;
1542 let distn = new_definition `!m n. distn m n = (m - n) + (n - m)`;;
1543
1544 (* Lemma distnC *)
1545 let distnC = section_proof ["m";"n"] `distn m n = distn n m` [
1546    (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1547 ];;
1548
1549 (* Lemma distn_add2l *)
1550 let distn_add2l = section_proof ["d";"m";"n"] `distn (d + m) (d + n) = distn m n` [
1551    (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_add2l")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1552 ];;
1553
1554 (* Lemma distn_add2r *)
1555 let distn_add2r = section_proof ["d";"m";"n"] `distn (m + d) (n + d) = distn m n` [
1556    (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_add2r")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1557 ];;
1558
1559 (* Lemma distnEr *)
1560 let distnEr = section_proof ["m";"n"] `m <= n ==> distn m n = n - m` [
1561    (BETA_TAC THEN (move ["le_m_n"]));
1562    (((((use_arg_then "distn")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then "EQ_IMP") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "leqE") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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_then "le_m_n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1563 ];;
1564
1565 (* Lemma distnEl *)
1566 let distnEl = section_proof ["m";"n"] `n <= m ==> distn m n = m - n` [
1567    ((BETA_TAC THEN (move ["le_n_m"])) THEN ((((use_arg_then "distnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1568 ];;
1569
1570 (* Lemma dist0n *)
1571 let dist0n = section_proof ["n"] `distn 0 n = n` [
1572    (((THENL) (((use_arg_then "n") (disch_tac [])) THEN (clear_assumption "n") THEN case) [ALL_TAC; (move ["m"])]) THEN ((((use_arg_then "distn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "sub0n")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "subn0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "add0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1573 ];;
1574
1575 (* Lemma distn0 *)
1576 let distn0 = section_proof ["n"] `distn n 0 = n` [
1577    (((((use_arg_then "distnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "dist0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1578 ];;
1579
1580 (* Lemma distnn *)
1581 let distnn = section_proof ["m"] `distn m m = 0` [
1582    (((repeat_tactic 1 9 (((use_arg_then "distn")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "subnn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn0")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1583 ];;
1584
1585 (* Lemma distn_eq0 *)
1586 let distn_eq0 = section_proof ["m";"n"] `(distn m n = 0) <=> (m = n)` [
1587    (((((use_arg_then "distn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "addn_eq0")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "subn_eq0")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "eqn_leq")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1588 ];;
1589
1590 (* Lemma distnS *)
1591 let distnS = section_proof ["m"] `distn m (SUC m) = 1` [
1592    ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "distn_add2r") (fun fst_arg -> (use_arg_then "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_then "add0n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "dist0n")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1593 ];;
1594
1595 (* Lemma distSn *)
1596 let distSn = section_proof ["m"] `distn (SUC m) m = 1` [
1597    (((((use_arg_then "distnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnS")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1598 ];;
1599
1600 (* Lemma distn_eq1 *)
1601 let distn_eq1 = section_proof ["m";"n"] `(distn m n = 1) <=> (if m < n then SUC m = n else m = SUC n)` [
1602    ((THENL) (((fun arg_tac -> (fun arg_tac -> (use_arg_then "ltnP") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(move ["lt_mn"]); (move ["le_mn"])]);
1603    (((((use_arg_then "eq_sym")(thm_tac (new_rewrite [] [(`_ = 1`)])))) THEN (((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "subnK")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "add1n")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1604    (((((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "distnEl")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "subnK")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "add1n")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "ltnNge")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "le_mn")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
1605 ];;
1606
1607 (* Lemma leqif_add_distn *)
1608 let leqif_add_distn = section_proof ["m";"n";"p"] `leqif (distn m p) (distn m n + distn n p) ((m <= n /\ n <= p) \/ (p <= n /\ n <= m))` [
1609    (((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"])))));
1610    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_total") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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_then "IH") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC));
1611    (((((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "orbC")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "distnC") (fun fst_arg -> (use_arg_then "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_then "distnC")(thm_tac (new_rewrite [] [(`distn p _`)])))))) THEN (done_tac));
1612    (BETA_TAC THEN (move ["m"]) THEN (move ["p"]) THEN (move ["le_mp"]));
1613    ((((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
1614    ((THENL) (((fun arg_tac -> (use_arg_then "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]);
1615    (((repeat_tactic 1 9 (((use_arg_then "distnEr")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "addnC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((fun arg_tac -> (use_arg_then "eqn_addr") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "addnA")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "subnK")(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1616    (((((use_arg_then "negb_and")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "ltnNge")(gsym_then (thm_tac (new_rewrite [] []))))))) THEN ALL_TAC THEN ((THENL) case [(move ["lt_nm"]); (move ["lt_pn"])]));
1617    (((fun arg_tac -> (fun arg_tac -> (use_arg_then "ltn_leq_trans") (fun fst_arg -> (use_arg_then "lt_nm") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "le_mp") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["lt_np"]));
1618    (((((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "lt_nm")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "lt_np")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "ltn_addl")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltn_sub2l")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1619    (((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_ltn_trans") (fun fst_arg -> (use_arg_then "le_mp") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "lt_pn") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (move ["lt_mn"]));
1620    (((((use_arg_then "leqifP")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "leqNgt")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "lt_mn")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "lt_pn")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "ltn_addr")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnEr")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "ltn_sub2r")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "ltnW")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1621 ];;
1622
1623 (* Lemma leq_add_distn *)
1624 let leq_add_distn = section_proof ["m";"n";"p"] `distn m p <= distn m n + distn n p` [
1625    ((((fun arg_tac -> (use_arg_then "leqif_imp_le") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "leqif_add_distn") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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));
1626 ];;
1627
1628 (* Lemma sqrn_distn *)
1629 let sqrn_distn = section_proof ["m";"n"] `(distn m n) ^ 2 + 2 * (m * n) = m ^ 2 + n ^ 2` [
1630    ((fun arg_tac -> arg_tac (Arg_term (`n <= m`))) (term_tac (wlog_tac (move ["le_nm"])[`m`; `n`])));
1631    (((fun arg_tac -> (fun arg_tac -> (use_arg_then "leq_total") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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_then "le_nm") (thm_tac (match_mp_then snd_th MP_TAC)))) THEN ((TRY done_tac)));
1632    (((((fun arg_tac -> (use_arg_then "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_then "mulnC") (fun fst_arg -> (use_arg_then "n") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "distnC")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1633    ((BETA_TAC THEN (move ["le_nm"])) THEN ((((use_arg_then "distnEl")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "sqrn_sub")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then "subnK")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then "leqif_imp_le") (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "nat_Cauchy") (fun fst_arg -> (use_arg_then "m") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "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));
1634 ];;