helm/software/matita/library/nat/gcd.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/primes.ma".
  16 include "nat/lt_arith.ma".
  17
  18 let rec gcd_aux p m n: nat \def
  19 match divides_b n m with
  20 [ true \Rightarrow n
  21 | false \Rightarrow
  22   match p with
  23   [O \Rightarrow n
  24   |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
  25
  26 definition gcd : nat \to nat \to nat \def
  27 \lambda n,m:nat.
  28   match leb n m with
  29   [ true \Rightarrow
  30     match n with
  31     [ O \Rightarrow m
  32     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
  33   | false \Rightarrow
  34     match m with
  35     [ O \Rightarrow n
  36     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
  37
  38 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
  39 p \divides (m \mod n).
  40 intros.elim H1.elim H2.
  41 (* apply (witness ? ? (n2 - n1*(m / n))). *)
  42 apply witness[|
  43 rewrite > distr_times_minus.
  44 rewrite < H3 in \vdash (? ? ? (? % ?)).
  45 rewrite < assoc_times.
  46 rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
  47 apply sym_eq.apply plus_to_minus.
  48 rewrite > sym_times.
  49 letin x \def div.
  50 rewrite < (div_mod ? ? H).
  51 reflexivity.
  52 ]
  53 qed.
  54
  55 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
  56 p \divides (m \mod n) \to p \divides n \to p \divides m.
  57 intros.elim H1.elim H2.
  58 apply (witness p m ((n2*(m / n))+n1)).
  59 rewrite > distr_times_plus.
  60 rewrite < H3.
  61 rewrite < assoc_times.
  62 rewrite < H4.rewrite < sym_times.
  63 apply div_mod.assumption.
  64 qed.
  65
  66 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
  67 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
  68 intro.elim p.
  69 absurd (O < n).assumption.apply le_to_not_lt.assumption.
  70 cut ((n1 \divides m) \lor (n1 \ndivides m)).
  71 simplify.
  72 elim Hcut.rewrite > divides_to_divides_b_true.
  73 simplify.
  74 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
  75 assumption.assumption.
  76 rewrite > not_divides_to_divides_b_false.
  77 simplify.
  78 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
  79 gcd_aux n n1 (m \mod n1) \divides mod m n1).
  80 elim Hcut1.
  81 split.apply (divides_mod_to_divides ? ? n1).
  82 assumption.assumption.assumption.assumption.
  83 apply H.
  84 cut (O \lt m \mod n1 \lor O = mod m n1).
  85 elim Hcut1.assumption.
  86 apply False_ind.apply H4.apply mod_O_to_divides.
  87 assumption.apply sym_eq.assumption.
  88 apply le_to_or_lt_eq.apply le_O_n.
  89 apply lt_to_le.
  90 apply lt_mod_m_m.assumption.
  91 apply le_S_S_to_le.
  92 apply (trans_le ? n1).
  93 change with (m \mod n1 < n1).
  94 apply lt_mod_m_m.assumption.assumption.
  95 assumption.assumption.
  96 apply (decidable_divides n1 m).assumption.
  97 qed.
  98
  99 theorem divides_gcd_nm: \forall n,m.
 100 gcd n m \divides m \land gcd n m \divides n.
 101 intros.
 102 change with
 103 (match leb n m with
 104   [ true \Rightarrow
 105     match n with
 106     [ O \Rightarrow m
 107     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 108   | false \Rightarrow
 109     match m with
 110     [ O \Rightarrow n
 111     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
 112 \land
 113 match leb n m with
 114   [ true \Rightarrow
 115     match n with
 116     [ O \Rightarrow m
 117     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 118   | false \Rightarrow
 119     match m with
 120     [ O \Rightarrow n
 121     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n).
 122 apply (leb_elim n m).
 123 apply (nat_case1 n).
 124 simplify.intros.split.
 125 apply (witness m m (S O)).apply times_n_SO.
 126 apply (witness m O O).apply times_n_O.
 127 intros.change with
 128 (gcd_aux (S m1) m (S m1) \divides m
 129 \land
 130 gcd_aux (S m1) m (S m1) \divides (S m1)).
 131 apply divides_gcd_aux_mn.
 132 unfold lt.apply le_S_S.apply le_O_n.
 133 assumption.apply le_n.
 134 simplify.intro.
 135 apply (nat_case1 m).
 136 simplify.intros.split.
 137 apply (witness n O O).apply times_n_O.
 138 apply (witness n n (S O)).apply times_n_SO.
 139 intros.change with
 140 (gcd_aux (S m1) n (S m1) \divides (S m1)
 141 \land
 142 gcd_aux (S m1) n (S m1) \divides n).
 143 cut (gcd_aux (S m1) n (S m1) \divides n
 144 \land
 145 gcd_aux (S m1) n (S m1) \divides S m1).
 146 elim Hcut.split.assumption.assumption.
 147 apply divides_gcd_aux_mn.
 148 unfold lt.apply le_S_S.apply le_O_n.
 149 apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.
 150 rewrite > H1.apply (trans_le ? (S n)).
 151 apply le_n_Sn.assumption.apply le_n.
 152 qed.
 153
 154 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
 155 intros.
 156 exact (proj2  ? ? (divides_gcd_nm n m)).
 157 qed.
 158
 159 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
 160 intros.
 161 exact (proj1 ? ? (divides_gcd_nm n m)).
 162 qed.
 163
 164
 165 theorem divides_times_gcd_aux: \forall p,m,n,d,c.
 166 O \lt c \to O < n \to n \le m \to n \le p \to
 167 d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n.
 168 intro.
 169 elim p
 170 [ absurd (O < n)
 171   [ assumption
 172   | apply le_to_not_lt.
 173     assumption
 174   ]
 175 | simplify.
 176   cut (n1 \divides m \lor n1 \ndivides m)
 177   [ elim Hcut
 178     [ rewrite > divides_to_divides_b_true
 179       [ simplify.
 180         assumption
 181       | assumption
 182       | assumption
 183       ]
 184     | rewrite > not_divides_to_divides_b_false
 185       [ simplify.
 186         apply H
 187         [ assumption
 188         | cut (O \lt m \mod n1 \lor O = m \mod n1)
 189           [ elim Hcut1
 190             [ assumption
 191             | absurd (n1 \divides m)
 192               [ apply mod_O_to_divides
 193                 [ assumption
 194                 | apply sym_eq.
 195                   assumption
 196                 ]
 197               | assumption
 198               ]
 199             ]
 200           | apply le_to_or_lt_eq.
 201             apply le_O_n
 202           ]
 203         | apply lt_to_le.
 204           apply lt_mod_m_m.
 205           assumption
 206         | apply le_S_S_to_le.
 207           apply (trans_le ? n1)
 208           [ change with (m \mod n1 < n1).
 209             apply lt_mod_m_m.
 210             assumption
 211           | assumption
 212           ]
 213         | assumption
 214         | rewrite < times_mod
 215           [ rewrite < (sym_times c m).
 216             rewrite < (sym_times c n1).
 217             apply divides_mod
 218             [ rewrite > (S_pred c)
 219               [ rewrite > (S_pred n1)
 220                 [ apply (lt_O_times_S_S)
 221                 | assumption
 222                 ]
 223               | assumption
 224               ]
 225             | assumption
 226             | assumption
 227             ]
 228           | assumption
 229           | assumption
 230           ]
 231         ]
 232       | assumption
 233       | assumption
 234       ]
 235     ]
 236   | apply (decidable_divides n1 m).
 237     assumption
 238   ]
 239 ]
 240 qed.
 241
 242 (*a particular case of the previous theorem (setting c=1)*)
 243 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 244 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
 245 intros.
 246 rewrite > (times_n_SO (gcd_aux p m n)).
 247 rewrite < (sym_times (S O)).
 248 apply (divides_times_gcd_aux)
 249 [ apply (lt_O_S O)
 250 | assumption
 251 | assumption
 252 | assumption
 253 | rewrite > (sym_times (S O)).
 254   rewrite < (times_n_SO m).
 255   assumption
 256 | rewrite > (sym_times (S O)).
 257   rewrite < (times_n_SO n).
 258   assumption
 259 ]
 260 qed.
 261
 262 theorem divides_d_times_gcd: \forall m,n,d,c.
 263 O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m.
 264 intros.
 265 change with
 266 (d \divides c *
 267 match leb n m with
 268   [ true \Rightarrow
 269     match n with
 270     [ O \Rightarrow m
 271     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 272   | false \Rightarrow
 273     match m with
 274     [ O \Rightarrow n
 275     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
 276 apply (leb_elim n m)
 277 [ apply (nat_case1 n)
 278   [ simplify.
 279     intros.
 280     assumption
 281   | intros.
 282     change with (d \divides c*gcd_aux (S m1) m (S m1)).
 283     apply divides_times_gcd_aux
 284     [ assumption
 285     | unfold lt.
 286       apply le_S_S.
 287       apply le_O_n
 288     | assumption
 289     | apply (le_n (S m1))
 290     | assumption
 291     | rewrite < H3.
 292       assumption
 293     ]
 294   ]
 295 | apply (nat_case1 m)
 296   [ simplify.
 297     intros.
 298     assumption
 299   | intros.
 300     change with (d \divides c * gcd_aux (S m1) n (S m1)).
 301     apply divides_times_gcd_aux
 302     [ unfold lt.
 303       change with (O \lt c).
 304       assumption
 305     | apply lt_O_S
 306     | apply lt_to_le.
 307       apply not_le_to_lt.
 308       assumption
 309     | apply (le_n (S m1)).
 310     | assumption
 311     | rewrite < H3.
 312       assumption
 313     ]
 314   ]
 315 ]
 316 qed.
 317
 318 (*a particular case of the previous theorem (setting c=1)*)
 319 theorem divides_d_gcd: \forall m,n,d.
 320 d \divides m \to d \divides n \to d \divides gcd n m.
 321 intros.
 322 rewrite > (times_n_SO (gcd n m)).
 323 rewrite < (sym_times (S O)).
 324 apply (divides_d_times_gcd)
 325 [ apply (lt_O_S O)
 326 | rewrite > (sym_times (S O)).
 327   rewrite < (times_n_SO m).
 328   assumption
 329 | rewrite > (sym_times (S O)).
 330   rewrite < (times_n_SO n).
 331   assumption
 332 ]
 333 qed.
 334
 335 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 336 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 337 intro.
 338 elim p
 339   [absurd (O < n)
 340     [assumption
 341     |apply le_to_not_lt.assumption
 342     ]
 343   |cut (O < m)
 344     [cut (n1 \divides m \lor  n1 \ndivides m)
 345       [simplify.
 346        elim Hcut1
 347         [rewrite > divides_to_divides_b_true
 348           [simplify.
 349            apply (ex_intro ? ? (S O)).
 350            apply (ex_intro ? ? O).
 351            left.
 352            simplify.
 353            rewrite < plus_n_O.
 354            apply sym_eq.
 355            apply minus_n_O
 356           |assumption
 357           |assumption
 358           ]
 359         |rewrite > not_divides_to_divides_b_false
 360           [change with
 361            (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
 362             \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
 363            cut
 364            (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
 365             \lor b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
 366             [elim Hcut2.elim H5.elim H6
 367               [(* first case *)
 368                rewrite < H7.
 369                apply (ex_intro ? ? (a1+a*(m / n1))).
 370                apply (ex_intro ? ? a).
 371                right.
 372                rewrite < sym_plus.
 373                rewrite < (sym_times n1).
 374                rewrite > distr_times_plus.
 375                rewrite > (sym_times n1).
 376                rewrite > (sym_times n1).
 377                rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?)
 378                 [rewrite > assoc_times.
 379                  rewrite < sym_plus.
 380                  rewrite > distr_times_plus.
 381                  rewrite < eq_minus_minus_minus_plus.
 382                  rewrite < sym_plus.
 383                  rewrite < plus_minus
 384                   [rewrite < minus_n_n.reflexivity
 385                   |apply le_n
 386                   ]
 387                 |assumption
 388                 ]
 389               |(* second case *)
 390               rewrite < H7.
 391                apply (ex_intro ? ? (a1+a*(m / n1))).
 392                apply (ex_intro ? ? a).
 393                left.
 394                (* clear Hcut2.clear H5.clear H6.clear H. *)
 395                rewrite > sym_times.
 396                rewrite > distr_times_plus.
 397                rewrite > sym_times.
 398                rewrite > (sym_times n1).
 399                rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
 400                 [rewrite > distr_times_plus.
 401                  rewrite > assoc_times.
 402                  rewrite < eq_minus_minus_minus_plus.
 403                  rewrite < sym_plus.
 404                  rewrite < plus_minus
 405                   [rewrite < minus_n_n.reflexivity
 406                   |apply le_n
 407                   ]
 408                 |assumption
 409                 ]
 410               ]
 411             |apply (H n1 (m \mod n1))
 412               [cut (O \lt m \mod n1 \lor O = m \mod n1)
 413                 [elim Hcut2
 414                   [assumption
 415                   |absurd (n1 \divides m)
 416                     [apply mod_O_to_divides
 417                       [assumption
 418                       |symmetry.assumption
 419                       ]
 420                     |assumption
 421                     ]
 422                   ]
 423                 |apply le_to_or_lt_eq.
 424                  apply le_O_n
 425                 ]
 426               |apply lt_to_le.
 427                apply lt_mod_m_m.
 428                assumption
 429               |apply le_S_S_to_le.
 430                apply (trans_le ? n1)
 431                 [change with (m \mod n1 < n1).
 432                  apply lt_mod_m_m.
 433                  assumption
 434                 |assumption
 435                 ]
 436               ]
 437             ]
 438           |assumption
 439           |assumption
 440           ]
 441         ]
 442       |apply (decidable_divides n1 m).
 443        assumption
 444       ]
 445     |apply (lt_to_le_to_lt ? n1);assumption
 446     ]
 447   ]
 448 qed.
 449
 450 theorem eq_minus_gcd:
 451  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 452 intros.
 453 unfold gcd.
 454 apply (leb_elim n m).
 455 apply (nat_case1 n).
 456 simplify.intros.
 457 apply (ex_intro ? ? O).
 458 apply (ex_intro ? ? (S O)).
 459 right.simplify.
 460 rewrite < plus_n_O.
 461 apply sym_eq.apply minus_n_O.
 462 intros.
 463 change with
 464 (\exists a,b.
 465 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 466 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 467 apply eq_minus_gcd_aux.
 468 unfold lt. apply le_S_S.apply le_O_n.
 469 assumption.apply le_n.
 470 apply (nat_case1 m).
 471 simplify.intros.
 472 apply (ex_intro ? ? (S O)).
 473 apply (ex_intro ? ? O).
 474 left.simplify.
 475 rewrite < plus_n_O.
 476 apply sym_eq.apply minus_n_O.
 477 intros.
 478 change with
 479 (\exists a,b.
 480 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 481 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
 482 cut
 483 (\exists a,b.
 484 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 485 \lor
 486 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
 487 elim Hcut.elim H2.elim H3.
 488 apply (ex_intro ? ? a1).
 489 apply (ex_intro ? ? a).
 490 right.assumption.
 491 apply (ex_intro ? ? a1).
 492 apply (ex_intro ? ? a).
 493 left.assumption.
 494 apply eq_minus_gcd_aux.
 495 unfold lt. apply le_S_S.apply le_O_n.
 496 apply lt_to_le.apply not_le_to_lt.assumption.
 497 apply le_n.
 498 qed.
 499
 500 (* some properties of gcd *)
 501
 502 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 503 intro.simplify.reflexivity.
 504 qed.
 505
 506 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 507 m = O \land n = O.
 508 intros.cut (O \divides n \land O \divides m).
 509 elim Hcut.elim H2.split.
 510 assumption.elim H1.assumption.
 511 rewrite < H.
 512 apply divides_gcd_nm.
 513 qed.
 514
 515 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
 516 intros.
 517 apply (nat_case1 (gcd m n)).
 518 intros.
 519 generalize in match (gcd_O_to_eq_O m n H1).
 520 intros.elim H2.
 521 rewrite < H4 in \vdash (? ? %).assumption.
 522 intros.unfold lt.apply le_S_S.apply le_O_n.
 523 qed.
 524
 525 theorem gcd_n_n: \forall n.gcd n n = n.
 526 intro.elim n
 527   [reflexivity
 528   |apply le_to_le_to_eq
 529     [apply divides_to_le
 530       [apply lt_O_S
 531       |apply divides_gcd_n
 532       ]
 533     |apply divides_to_le
 534       [apply lt_O_gcd.apply lt_O_S
 535       |apply divides_d_gcd
 536         [apply divides_n_n|apply divides_n_n]
 537       ]
 538     ]
 539   ]
 540 qed.
 541
 542 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
 543 O < i.
 544 intros.
 545 elim (le_to_or_lt_eq ? ? (le_O_n i))
 546   [assumption
 547   |absurd ((gcd i n) = (S O))
 548     [assumption
 549     |rewrite < H2.
 550      simplify.
 551      unfold.intro.
 552      apply (lt_to_not_eq (S O) n H).
 553      apply sym_eq.assumption
 554     ]
 555   ]
 556 qed.
 557
 558 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
 559 i < n.
 560 intros.
 561 elim (le_to_or_lt_eq ? ? H1)
 562   [assumption
 563   |absurd ((gcd i n) = (S O))
 564     [assumption
 565     |rewrite > H3.
 566      rewrite > gcd_n_n.
 567      unfold.intro.
 568      apply (lt_to_not_eq (S O) n H).
 569      apply sym_eq.assumption
 570     ]
 571   ]
 572 qed.
 573
 574 theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
 575 intro.apply (nat_case n)
 576   [intros.reflexivity
 577   |intros.
 578    apply le_to_le_to_eq
 579     [apply divides_to_le
 580       [apply lt_O_S|apply divides_gcd_n]
 581     |apply divides_to_le
 582       [apply lt_O_gcd.rewrite > (times_n_O O).
 583        apply lt_times[apply lt_O_S|assumption]
 584       |apply divides_d_gcd
 585         [apply (witness ? ? m1).reflexivity
 586         |apply divides_n_n
 587         ]
 588       ]
 589     ]
 590   ]
 591 qed.
 592
 593 theorem symmetric_gcd: symmetric nat gcd.
 594 change with
 595 (\forall n,m:nat. gcd n m = gcd m n).
 596 intros.
 597 cut (O < (gcd n m) \lor O = (gcd n m)).
 598 elim Hcut.
 599 cut (O < (gcd m n) \lor O = (gcd m n)).
 600 elim Hcut1.
 601 apply antisym_le.
 602 apply divides_to_le.assumption.
 603 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 604 apply divides_to_le.assumption.
 605 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 606 rewrite < H1.
 607 cut (m=O \land n=O).
 608 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
 609 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 610 apply le_to_or_lt_eq.apply le_O_n.
 611 rewrite < H.
 612 cut (n=O \land m=O).
 613 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
 614 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 615 apply le_to_or_lt_eq.apply le_O_n.
 616 qed.
 617
 618 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 619 symmetric_gcd.
 620
 621 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
 622 intros.
 623 apply (nat_case n).apply le_n.
 624 intro.
 625 apply divides_to_le.
 626 apply lt_O_gcd.
 627 rewrite > (times_n_O O).
 628 apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
 629 apply divides_d_gcd.
 630 apply (transitive_divides ? (S m1)).
 631 apply divides_gcd_m.
 632 apply (witness ? ? p).reflexivity.
 633 apply divides_gcd_n.
 634 qed.
 635
 636 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
 637 gcd m (n*p) = (S O) \to gcd m n = (S O).
 638 intros.
 639 apply antisymmetric_le.
 640 rewrite < H2.
 641 apply le_gcd_times.assumption.
 642 change with (O < gcd m n).
 643 apply lt_O_gcd.assumption.
 644 qed.
 645
 646 (* for the "converse" of the previous result see the end  of this development *)
 647
 648 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
 649 (gcd n m) = (S O) \to \lnot (divides n m).
 650 intros.unfold.intro.
 651 elim H2.
 652 generalize in match H1.
 653 rewrite > H3.
 654 intro.
 655 cut (O < n1)
 656   [elim (gcd_times_SO_to_gcd_SO n n n1 ? ? H4)
 657     [cut (gcd n (n*n1) = n)
 658       [apply (lt_to_not_eq (S O) n)
 659         [assumption|rewrite < H4.assumption]
 660       |apply gcd_n_times_nm.assumption
 661       ]
 662     |apply (trans_lt ? (S O))[apply le_n|assumption]
 663     |assumption
 664     ]
 665   |elim (le_to_or_lt_eq O n1 (le_O_n n1));
 666     [assumption
 667     |apply False_ind.
 668      apply (le_to_not_lt n (S O))
 669       [rewrite < H4.
 670        apply divides_to_le
 671         [rewrite > H4.apply lt_O_S
 672         |apply divides_d_gcd
 673           [apply (witness ? ? n1).reflexivity
 674           |apply divides_n_n
 675           ]
 676         ]
 677       |assumption
 678       ]
 679     ]
 680   ]
 681 qed.
 682
 683 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 684 intro.
 685 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
 686 apply divides_gcd_n.
 687 cut (O < gcd (S O) n \lor O = gcd (S O) n).
 688 elim Hcut.assumption.
 689 apply False_ind.
 690 apply (not_eq_O_S O).
 691 cut ((S O)=O \land n=O).
 692 elim Hcut1.apply sym_eq.assumption.
 693 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 694 apply le_to_or_lt_eq.apply le_O_n.
 695 qed.
 696
 697 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
 698 divides (gcd m n) (gcd n (m \mod n)).
 699 intros.
 700 apply divides_d_gcd.
 701 apply divides_mod.assumption.
 702 apply divides_gcd_n.
 703 apply divides_gcd_m.
 704 apply divides_gcd_m.
 705 qed.
 706
 707 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
 708 divides (gcd n (m \mod n)) (gcd m n) .
 709 intros.
 710 apply divides_d_gcd.
 711 apply divides_gcd_n.
 712 apply (divides_mod_to_divides ? ? n).
 713 assumption.
 714 apply divides_gcd_m.
 715 apply divides_gcd_n.
 716 qed.
 717
 718 theorem gcd_mod: \forall m,n:nat. O < n \to
 719 (gcd n (m \mod n)) = (gcd m n) .
 720 intros.
 721 apply antisymmetric_divides.
 722 apply divides_mod_gcd.assumption.
 723 apply divides_gcd_mod.assumption.
 724 qed.
 725
 726 (* gcd and primes *)
 727
 728 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 729 gcd n m = (S O).
 730 intros.unfold prime in H.
 731 elim H.
 732 apply antisym_le.
 733 apply not_lt_to_le.unfold Not.unfold lt.
 734 intro.
 735 apply H1.rewrite < (H3 (gcd n m)).
 736 apply divides_gcd_m.
 737 apply divides_gcd_n.assumption.
 738 cut (O < gcd n m \lor O = gcd n m).
 739 elim Hcut.assumption.
 740 apply False_ind.
 741 apply (not_le_Sn_O (S O)).
 742 cut (n=O \land m=O).
 743 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
 744 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 745 apply le_to_or_lt_eq.apply le_O_n.
 746 qed.
 747
 748 (* primes and divides *)
 749 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 750 n \divides p \lor n \divides q.
 751 intros.
 752 cut (n \divides p \lor n \ndivides p)
 753   [elim Hcut
 754     [left.assumption
 755     |right.
 756      cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
 757        [elim Hcut1.elim H3.elim H4
 758          [(* first case *)
 759           rewrite > (times_n_SO q).rewrite < H5.
 760           rewrite > distr_times_minus.
 761           rewrite > (sym_times q (a1*p)).
 762           rewrite > (assoc_times a1).
 763           elim H1.
 764           pump 39.
 765           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
 766           (*
 767           rewrite < (sym_times n).rewrite < assoc_times.
 768           rewrite > (sym_times q).rewrite > assoc_times.
 769           rewrite < (assoc_times a1).rewrite < (sym_times n).
 770           rewrite > (assoc_times n).
 771           rewrite < distr_times_minus.
 772           apply (witness ? ? (q*a-a1*n2)).reflexivity
 773           *)
 774          |(* second case *)
 775           rewrite > (times_n_SO q).rewrite < H5.
 776           rewrite > distr_times_minus.
 777           rewrite > (sym_times q (a1*p)).
 778           rewrite > (assoc_times a1).
 779           elim H1.rewrite > H6.
 780           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
 781           (*
 782           rewrite < sym_times.rewrite > assoc_times.
 783           rewrite < (assoc_times q).
 784           rewrite < (sym_times n).
 785           rewrite < distr_times_minus.
 786           apply (witness ? ? (n1*a1-q*a)).reflexivity
 787           *)
 788         ](* end second case *)
 789      |rewrite < (prime_to_gcd_SO n p)
 790        [apply eq_minus_gcd|assumption|assumption
 791        ]
 792      ]
 793    ]
 794  |apply (decidable_divides n p).
 795   apply (trans_lt ? (S O))
 796     [unfold lt.apply le_n
 797     |unfold prime in H.elim H. assumption
 798     ]
 799   ]
 800 qed.
 801
 802 theorem divides_exp_to_divides:
 803 \forall p,n,m:nat. prime p \to
 804 p \divides n \sup m \to p \divides n.
 805 intros 3.elim m.simplify in H1.
 806 apply (transitive_divides p (S O)).assumption.
 807 apply divides_SO_n.
 808 cut (p \divides n \lor p \divides n \sup n1).
 809 elim Hcut.assumption.
 810 apply H.assumption.assumption.
 811 apply divides_times_to_divides.assumption.
 812 exact H2.
 813 qed.
 814
 815 theorem divides_exp_to_eq:
 816 \forall p,q,m:nat. prime p \to prime q \to
 817 p \divides q \sup m \to p = q.
 818 intros.
 819 unfold prime in H1.
 820 elim H1.apply H4.
 821 apply (divides_exp_to_divides p q m).
 822 assumption.assumption.
 823 unfold prime in H.elim H.assumption.
 824 qed.
 825
 826 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
 827 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
 828 intros.
 829 apply antisymmetric_le.
 830 apply not_lt_to_le.
 831 unfold Not.intro.
 832 cut (divides (smallest_factor (gcd m (n*p))) n \lor
 833      divides (smallest_factor (gcd m (n*p))) p).
 834 elim Hcut.
 835 apply (not_le_Sn_n (S O)).
 836 change with ((S O) < (S O)).
 837 rewrite < H2 in \vdash (? ? %).
 838 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 839 apply lt_SO_smallest_factor.assumption.
 840 apply divides_to_le.
 841 rewrite > H2.unfold lt.apply le_n.
 842 apply divides_d_gcd.assumption.
 843 apply (transitive_divides ? (gcd m (n*p))).
 844 apply divides_smallest_factor_n.
 845 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 846 apply divides_gcd_n.
 847 apply (not_le_Sn_n (S O)).
 848 change with ((S O) < (S O)).
 849 rewrite < H3 in \vdash (? ? %).
 850 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 851 apply lt_SO_smallest_factor.assumption.
 852 apply divides_to_le.
 853 rewrite > H3.unfold lt.apply le_n.
 854 apply divides_d_gcd.assumption.
 855 apply (transitive_divides ? (gcd m (n*p))).
 856 apply divides_smallest_factor_n.
 857 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 858 apply divides_gcd_n.
 859 apply divides_times_to_divides.
 860 apply prime_smallest_factor_n.
 861 assumption.
 862 apply (transitive_divides ? (gcd m (n*p))).
 863 apply divides_smallest_factor_n.
 864 apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
 865 apply divides_gcd_m.
 866 change with (O < gcd m (n*p)).
 867 apply lt_O_gcd.
 868 rewrite > (times_n_O O).
 869 apply lt_times.assumption.assumption.
 870 qed.
 871
 872 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
 873 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
 874 intros.
 875 cut (n \divides p \lor n \ndivides p)
 876   [elim Hcut
 877     [assumption
 878     |cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
 879       [elim Hcut1.elim H4.elim H5
 880         [(* first case *)
 881           rewrite > (times_n_SO p).rewrite < H6.
 882           rewrite > distr_times_minus.
 883           rewrite > (sym_times p (a1*m)).
 884           rewrite > (assoc_times a1).
 885           elim H2.rewrite > H7.
 886           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
 887          |(* second case *)
 888           rewrite > (times_n_SO p).rewrite < H6.
 889           rewrite > distr_times_minus.
 890           rewrite > (sym_times p (a1*m)).
 891           rewrite > (assoc_times a1).
 892           elim H2.rewrite > H7.
 893           applyS (witness n ? ? (refl_eq ? ?)).
 894         ](* end second case *)
 895      |rewrite < H1.apply eq_minus_gcd.
 896      ]
 897    ]
 898  |apply (decidable_divides n p).
 899   assumption.
 900  ]
 901 qed.
 902
 903 (*
 904 theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
 905 divides p n \to divides q n \to divides (p*q) n.
 906 intros.elim H3.
 907 rewrite > H5 in H4.
 908 elim (divides_times_to_divides ? ? ? H1 H4)
 909   [elim H.apply False_ind.
 910    apply H2.apply sym_eq.apply H8
 911     [assumption
 912     |apply prime_to_lt_SO.assumption
 913     ]
 914   |elim H6.
 915    apply (witness ? ? n1).
 916    rewrite > assoc_times.
 917    rewrite < H7.assumption
 918   ]
 919 qed.
 920 *)
 921
 922 theorem divides_to_divides_times: \forall p,q,n. prime p  \to p \ndivides q \to
 923 divides p n \to divides q n \to divides (p*q) n.
 924 intros.elim H3.
 925 rewrite > H4 in H2.
 926 elim (divides_times_to_divides ? ? ? H H2)
 927   [apply False_ind.apply H1.assumption
 928   |elim H5.
 929    apply (witness ? ? n2).
 930    rewrite > sym_times in ⊢ (? ? ? (? % ?)).
 931    rewrite > assoc_times.
 932    rewrite < H6.assumption
 933   ]
 934 qed.