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