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
  19 let rec gcd_aux p m n: nat \def
  20 match divides_b n m with
  21 [ true \Rightarrow n
  22 | false \Rightarrow
  23   match p with
  24   [O \Rightarrow n
  25   |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
  26
  27 definition gcd : nat \to nat \to nat \def
  28 \lambda n,m:nat.
  29   match leb n m with
  30   [ true \Rightarrow
  31     match n with
  32     [ O \Rightarrow m
  33     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
  34   | false \Rightarrow
  35     match m with
  36     [ O \Rightarrow n
  37     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
  38
  39 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
  40 p \divides (m \mod n).
  41 intros.elim H1.elim H2.
  42 apply (witness ? ? (n2 - n1*(m / n))).
  43 rewrite > distr_times_minus.
  44 rewrite < H3.
  45 rewrite < assoc_times.
  46 rewrite < H4.
  47 apply sym_eq.
  48 apply plus_to_minus.
  49 rewrite > sym_times.
  50 apply div_mod.
  51 assumption.
  52 qed.
  53
  54 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
  55 p \divides (m \mod n) \to p \divides n \to p \divides m.
  56 intros.elim H1.elim H2.
  57 apply (witness p m ((n1*(m / n))+n2)).
  58 rewrite > distr_times_plus.
  59 rewrite < H3.
  60 rewrite < assoc_times.
  61 rewrite < H4.rewrite < sym_times.
  62 apply div_mod.assumption.
  63 qed.
  64
  65 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
  66 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
  67 intro.elim p.
  68 absurd (O < n).assumption.apply le_to_not_lt.assumption.
  69 cut ((n1 \divides m) \lor (n1 \ndivides m)).
  70 simplify.
  71 elim Hcut.rewrite > divides_to_divides_b_true.
  72 simplify.
  73 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
  74 assumption.assumption.
  75 rewrite > not_divides_to_divides_b_false.
  76 simplify.
  77 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
  78 gcd_aux n n1 (m \mod n1) \divides mod m n1).
  79 elim Hcut1.
  80 split.apply (divides_mod_to_divides ? ? n1).
  81 assumption.assumption.assumption.assumption.
  82 apply H.
  83 cut (O \lt m \mod n1 \lor O = mod m n1).
  84 elim Hcut1.assumption.
  85 apply False_ind.apply H4.apply mod_O_to_divides.
  86 assumption.apply sym_eq.assumption.
  87 apply le_to_or_lt_eq.apply le_O_n.
  88 apply lt_to_le.
  89 apply lt_mod_m_m.assumption.
  90 apply le_S_S_to_le.
  91 apply (trans_le ? n1).
  92 change with (m \mod n1 < n1).
  93 apply lt_mod_m_m.assumption.assumption.
  94 assumption.assumption.
  95 apply (decidable_divides n1 m).assumption.
  96 qed.
  97
  98 theorem divides_gcd_nm: \forall n,m.
  99 gcd n m \divides m \land gcd n m \divides n.
 100 intros.
 101 (*CSC: simplify simplifies too much because of a redex in gcd *)
 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 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 165 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
 166 intro.elim p.
 167 absurd (O < n).assumption.apply le_to_not_lt.assumption.
 168 simplify.
 169 cut (n1 \divides m \lor n1 \ndivides m).
 170 elim Hcut.
 171 rewrite > divides_to_divides_b_true.
 172 simplify.assumption.
 173 assumption.assumption.
 174 rewrite > not_divides_to_divides_b_false.
 175 simplify.
 176 apply H.
 177 cut (O \lt m \mod n1 \lor O = m \mod n1).
 178 elim Hcut1.assumption.
 179 absurd (n1 \divides m).apply mod_O_to_divides.
 180 assumption.apply sym_eq.assumption.assumption.
 181 apply le_to_or_lt_eq.apply le_O_n.
 182 apply lt_to_le.
 183 apply lt_mod_m_m.assumption.
 184 apply le_S_S_to_le.
 185 apply (trans_le ? n1).
 186 change with (m \mod n1 < n1).
 187 apply lt_mod_m_m.assumption.assumption.
 188 assumption.
 189 apply divides_mod.assumption.assumption.assumption.
 190 assumption.assumption.
 191 apply (decidable_divides n1 m).assumption.
 192 qed.
 193
 194 theorem divides_d_gcd: \forall m,n,d.
 195 d \divides m \to d \divides n \to d \divides gcd n m.
 196 intros.
 197 (*CSC: here simplify simplifies too much because of a redex in gcd *)
 198 change with
 199 (d \divides
 200 match leb n m with
 201   [ true \Rightarrow
 202     match n with
 203     [ O \Rightarrow m
 204     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 205   | false \Rightarrow
 206     match m with
 207     [ O \Rightarrow n
 208     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
 209 apply (leb_elim n m).
 210 apply (nat_case1 n).simplify.intros.assumption.
 211 intros.
 212 change with (d \divides gcd_aux (S m1) m (S m1)).
 213 apply divides_gcd_aux.
 214 unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
 215 rewrite < H2.assumption.
 216 apply (nat_case1 m).simplify.intros.assumption.
 217 intros.
 218 change with (d \divides gcd_aux (S m1) n (S m1)).
 219 apply divides_gcd_aux.
 220 unfold lt.apply le_S_S.apply le_O_n.
 221 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 222 rewrite < H2.assumption.
 223 qed.
 224
 225 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 226 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 227 intro.
 228 elim p.
 229 absurd (O < n).assumption.apply le_to_not_lt.assumption.
 230 cut (O < m).
 231 cut (n1 \divides m \lor  n1 \ndivides m).
 232 simplify.
 233 elim Hcut1.
 234 rewrite > divides_to_divides_b_true.
 235 simplify.
 236 apply (ex_intro ? ? (S O)).
 237 apply (ex_intro ? ? O).
 238 left.simplify.rewrite < plus_n_O.
 239 apply sym_eq.apply minus_n_O.
 240 assumption.assumption.
 241 rewrite > not_divides_to_divides_b_false.
 242 change with
 243 (\exists a,b.
 244 a*n1 - b*m = gcd_aux n n1 (m \mod n1)
 245 \lor
 246 b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
 247 cut
 248 (\exists a,b.
 249 a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
 250 \lor
 251 b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
 252 elim Hcut2.elim H5.elim H6.
 253 (* first case *)
 254 rewrite < H7.
 255 apply (ex_intro ? ? (a1+a*(m / n1))).
 256 apply (ex_intro ? ? a).
 257 right.
 258 rewrite < sym_plus.
 259 rewrite < (sym_times n1).
 260 rewrite > distr_times_plus.
 261 rewrite > (sym_times n1).
 262 rewrite > (sym_times n1).
 263 rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
 264 rewrite > assoc_times.
 265 rewrite < sym_plus.
 266 rewrite > distr_times_plus.
 267 rewrite < eq_minus_minus_minus_plus.
 268 rewrite < sym_plus.
 269 rewrite < plus_minus.
 270 rewrite < minus_n_n.reflexivity.
 271 apply le_n.
 272 assumption.
 273 (* second case *)
 274 rewrite < H7.
 275 apply (ex_intro ? ? (a1+a*(m / n1))).
 276 apply (ex_intro ? ? a).
 277 left.
 278 (* clear Hcut2.clear H5.clear H6.clear H. *)
 279 rewrite > sym_times.
 280 rewrite > distr_times_plus.
 281 rewrite > sym_times.
 282 rewrite > (sym_times n1).
 283 rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
 284 rewrite > distr_times_plus.
 285 rewrite > assoc_times.
 286 rewrite < eq_minus_minus_minus_plus.
 287 rewrite < sym_plus.
 288 rewrite < plus_minus.
 289 rewrite < minus_n_n.reflexivity.
 290 apply le_n.
 291 assumption.
 292 apply (H n1 (m \mod n1)).
 293 cut (O \lt m \mod n1 \lor O = m \mod n1).
 294 elim Hcut2.assumption.
 295 absurd (n1 \divides m).apply mod_O_to_divides.
 296 assumption.
 297 symmetry.assumption.assumption.
 298 apply le_to_or_lt_eq.apply le_O_n.
 299 apply lt_to_le.
 300 apply lt_mod_m_m.assumption.
 301 apply le_S_S_to_le.
 302 apply (trans_le ? n1).
 303 change with (m \mod n1 < n1).
 304 apply lt_mod_m_m.
 305 assumption.assumption.assumption.assumption.
 306 apply (decidable_divides n1 m).assumption.
 307 apply (lt_to_le_to_lt ? n1).assumption.assumption.
 308 qed.
 309
 310 theorem eq_minus_gcd:
 311  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 312 intros.
 313 unfold gcd.
 314 apply (leb_elim n m).
 315 apply (nat_case1 n).
 316 simplify.intros.
 317 apply (ex_intro ? ? O).
 318 apply (ex_intro ? ? (S O)).
 319 right.simplify.
 320 rewrite < plus_n_O.
 321 apply sym_eq.apply minus_n_O.
 322 intros.
 323 change with
 324 (\exists a,b.
 325 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 326 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 327 apply eq_minus_gcd_aux.
 328 unfold lt. apply le_S_S.apply le_O_n.
 329 assumption.apply le_n.
 330 apply (nat_case1 m).
 331 simplify.intros.
 332 apply (ex_intro ? ? (S O)).
 333 apply (ex_intro ? ? O).
 334 left.simplify.
 335 rewrite < plus_n_O.
 336 apply sym_eq.apply minus_n_O.
 337 intros.
 338 change with
 339 (\exists a,b.
 340 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 341 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
 342 cut
 343 (\exists a,b.
 344 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 345 \lor
 346 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
 347 elim Hcut.elim H2.elim H3.
 348 apply (ex_intro ? ? a1).
 349 apply (ex_intro ? ? a).
 350 right.assumption.
 351 apply (ex_intro ? ? a1).
 352 apply (ex_intro ? ? a).
 353 left.assumption.
 354 apply eq_minus_gcd_aux.
 355 unfold lt. apply le_S_S.apply le_O_n.
 356 apply lt_to_le.apply not_le_to_lt.assumption.
 357 apply le_n.
 358 qed.
 359
 360 (* some properties of gcd *)
 361
 362 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 363 intro.simplify.reflexivity.
 364 qed.
 365
 366 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 367 m = O \land n = O.
 368 intros.cut (O \divides n \land O \divides m).
 369 elim Hcut.elim H2.split.
 370 assumption.elim H1.assumption.
 371 rewrite < H.
 372 apply divides_gcd_nm.
 373 qed.
 374
 375 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
 376 intros.
 377 apply (nat_case1 (gcd m n)).
 378 intros.
 379 generalize in match (gcd_O_to_eq_O m n H1).
 380 intros.elim H2.
 381 rewrite < H4 in \vdash (? ? %).assumption.
 382 intros.unfold lt.apply le_S_S.apply le_O_n.
 383 qed.
 384
 385 theorem symmetric_gcd: symmetric nat gcd.
 386 (*CSC: bug here: unfold symmetric does not work *)
 387 change with
 388 (\forall n,m:nat. gcd n m = gcd m n).
 389 intros.
 390 cut (O < (gcd n m) \lor O = (gcd n m)).
 391 elim Hcut.
 392 cut (O < (gcd m n) \lor O = (gcd m n)).
 393 elim Hcut1.
 394 apply antisym_le.
 395 apply divides_to_le.assumption.
 396 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 397 apply divides_to_le.assumption.
 398 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 399 rewrite < H1.
 400 cut (m=O \land n=O).
 401 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
 402 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 403 apply le_to_or_lt_eq.apply le_O_n.
 404 rewrite < H.
 405 cut (n=O \land m=O).
 406 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
 407 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 408 apply le_to_or_lt_eq.apply le_O_n.
 409 qed.
 410
 411 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 412 symmetric_gcd.
 413
 414 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
 415 intros.
 416 apply (nat_case n).reflexivity.
 417 intro.
 418 apply divides_to_le.
 419 apply lt_O_gcd.
 420 rewrite > (times_n_O O).
 421 apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
 422 apply divides_d_gcd.
 423 apply (transitive_divides ? (S m1)).
 424 apply divides_gcd_m.
 425 apply (witness ? ? p).reflexivity.
 426 apply divides_gcd_n.
 427 qed.
 428
 429 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
 430 gcd m (n*p) = (S O) \to gcd m n = (S O).
 431 intros.
 432 apply antisymmetric_le.
 433 rewrite < H2.
 434 apply le_gcd_times.assumption.
 435 change with (O < gcd m n).
 436 apply lt_O_gcd.assumption.
 437 qed.
 438
 439 (* for the "converse" of the previous result see the end  of this development *)
 440
 441 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 442 intro.
 443 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
 444 apply divides_gcd_n.
 445 cut (O < gcd (S O) n \lor O = gcd (S O) n).
 446 elim Hcut.assumption.
 447 apply False_ind.
 448 apply (not_eq_O_S O).
 449 cut ((S O)=O \land n=O).
 450 elim Hcut1.apply sym_eq.assumption.
 451 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 452 apply le_to_or_lt_eq.apply le_O_n.
 453 qed.
 454
 455 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
 456 divides (gcd m n) (gcd n (m \mod n)).
 457 intros.
 458 apply divides_d_gcd.
 459 apply divides_mod.assumption.
 460 apply divides_gcd_n.
 461 apply divides_gcd_m.
 462 apply divides_gcd_m.
 463 qed.
 464
 465 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
 466 divides (gcd n (m \mod n)) (gcd m n) .
 467 intros.
 468 apply divides_d_gcd.
 469 apply divides_gcd_n.
 470 apply (divides_mod_to_divides ? ? n).
 471 assumption.
 472 apply divides_gcd_m.
 473 apply divides_gcd_n.
 474 qed.
 475
 476 theorem gcd_mod: \forall m,n:nat. O < n \to
 477 (gcd n (m \mod n)) = (gcd m n) .
 478 intros.
 479 apply antisymmetric_divides.
 480 apply divides_mod_gcd.assumption.
 481 apply divides_gcd_mod.assumption.
 482 qed.
 483
 484 (* gcd and primes *)
 485
 486 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 487 gcd n m = (S O).
 488 intros.unfold prime in H.
 489 elim H.
 490 apply antisym_le.
 491 apply not_lt_to_le.unfold Not.unfold lt.
 492 intro.
 493 apply H1.rewrite < (H3 (gcd n m)).
 494 apply divides_gcd_m.
 495 apply divides_gcd_n.assumption.
 496 cut (O < gcd n m \lor O = gcd n m).
 497 elim Hcut.assumption.
 498 apply False_ind.
 499 apply (not_le_Sn_O (S O)).
 500 cut (n=O \land m=O).
 501 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
 502 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 503 apply le_to_or_lt_eq.apply le_O_n.
 504 qed.
 505
 506 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 507 n \divides p \lor n \divides q.
 508 intros.
 509 cut (n \divides p \lor n \ndivides p).
 510 elim Hcut.
 511 left.assumption.
 512 right.
 513 cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O)).
 514 elim Hcut1.elim H3.elim H4.
 515 (* first case *)
 516 rewrite > (times_n_SO q).rewrite < H5.
 517 rewrite > distr_times_minus.
 518 rewrite > (sym_times q (a1*p)).
 519 rewrite > (assoc_times a1).
 520 elim H1.rewrite > H6.
 521 rewrite < (sym_times n).rewrite < assoc_times.
 522 rewrite > (sym_times q).rewrite > assoc_times.
 523 rewrite < (assoc_times a1).rewrite < (sym_times n).
 524 rewrite > (assoc_times n).
 525 rewrite < distr_times_minus.
 526 apply (witness ? ? (q*a-a1*n2)).reflexivity.
 527 (* second case *)
 528 rewrite > (times_n_SO q).rewrite < H5.
 529 rewrite > distr_times_minus.
 530 rewrite > (sym_times q (a1*p)).
 531 rewrite > (assoc_times a1).
 532 elim H1.rewrite > H6.
 533 rewrite < sym_times.rewrite > assoc_times.
 534 rewrite < (assoc_times q).
 535 rewrite < (sym_times n).
 536 rewrite < distr_times_minus.
 537 apply (witness ? ? (n2*a1-q*a)).reflexivity.
 538 (* end second case *)
 539 rewrite < (prime_to_gcd_SO n p).
 540 apply eq_minus_gcd.
 541 assumption.assumption.
 542 apply (decidable_divides n p).
 543 apply (trans_lt ? (S O)).unfold lt.apply le_n.
 544 unfold prime in H.elim H. assumption.
 545 qed.
 546
 547 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
 548 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
 549 intros.
 550 apply antisymmetric_le.
 551 apply not_lt_to_le.
 552 unfold Not.intro.
 553 cut (divides (smallest_factor (gcd m (n*p))) n \lor
 554      divides (smallest_factor (gcd m (n*p))) p).
 555 elim Hcut.
 556 apply (not_le_Sn_n (S O)).
 557 change with ((S O) < (S O)).
 558 rewrite < H2 in \vdash (? ? %).
 559 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 560 apply lt_SO_smallest_factor.assumption.
 561 apply divides_to_le.
 562 rewrite > H2.unfold lt.apply le_n.
 563 apply divides_d_gcd.assumption.
 564 apply (transitive_divides ? (gcd m (n*p))).
 565 apply divides_smallest_factor_n.
 566 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 567 apply divides_gcd_n.
 568 apply (not_le_Sn_n (S O)).
 569 change with ((S O) < (S O)).
 570 rewrite < H3 in \vdash (? ? %).
 571 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 572 apply lt_SO_smallest_factor.assumption.
 573 apply divides_to_le.
 574 rewrite > H3.unfold lt.apply le_n.
 575 apply divides_d_gcd.assumption.
 576 apply (transitive_divides ? (gcd m (n*p))).
 577 apply divides_smallest_factor_n.
 578 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 579 apply divides_gcd_n.
 580 apply divides_times_to_divides.
 581 apply prime_smallest_factor_n.
 582 assumption.
 583 apply (transitive_divides ? (gcd m (n*p))).
 584 apply divides_smallest_factor_n.
 585 apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
 586 apply divides_gcd_m.
 587 change with (O < gcd m (n*p)).
 588 apply lt_O_gcd.
 589 rewrite > (times_n_O O).
 590 apply lt_times.assumption.assumption.
 591 qed.