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