]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/gcd.ma
fix
[helm.git] / 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.