]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/primes.ma
removed a pointless call to auto
[helm.git] / matita / library / nat / primes.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/primes".
16
17 include "nat/div_and_mod.ma".
18 include "nat/minimization.ma".
19 include "nat/sigma_and_pi.ma".
20 include "nat/factorial.ma".
21
22 inductive divides (n,m:nat) : Prop \def
23 witness : \forall p:nat.m = times n p \to divides n m.
24
25 interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m).
26 interpretation "not divides" 'ndivides n m =
27  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
28
29 theorem reflexive_divides : reflexive nat divides.
30 unfold reflexive.
31 intros.
32 exact (witness x x (S O) (times_n_SO x)).
33 qed.
34
35 theorem divides_to_div_mod_spec :
36 \forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O.
37 intros.elim H1.rewrite > H2.
38 constructor 1.assumption.
39 apply (lt_O_n_elim n H).intros.
40 rewrite < plus_n_O.
41 rewrite > div_times.apply sym_times.
42 qed.
43
44 theorem div_mod_spec_to_divides :
45 \forall n,m,p. div_mod_spec m n p O \to n \divides m.
46 intros.elim H.
47 apply (witness n m p).
48 rewrite < sym_times.
49 rewrite > (plus_n_O (p*n)).assumption.
50 qed.
51
52 theorem divides_to_mod_O:
53 \forall n,m. O < n \to n \divides m \to (m \mod n) = O.
54 intros.apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O).
55 apply div_mod_spec_div_mod.assumption.
56 apply divides_to_div_mod_spec.assumption.assumption.
57 qed.
58
59 theorem mod_O_to_divides:
60 \forall n,m. O< n \to (m \mod n) = O \to  n \divides m.
61 intros.
62 apply (witness n m (m / n)).
63 rewrite > (plus_n_O (n * (m / n))).
64 rewrite < H1.
65 rewrite < sym_times.
66 (* Andrea: perche' hint non lo trova ?*)
67 apply div_mod.
68 assumption.
69 qed.
70
71 theorem divides_n_O: \forall n:nat. n \divides O.
72 intro. apply (witness n O O).apply times_n_O.
73 qed.
74
75 theorem divides_n_n: \forall n:nat. n \divides n.
76 intro. apply (witness n n (S O)).apply times_n_SO.
77 qed.
78
79 theorem divides_SO_n: \forall n:nat. (S O) \divides n.
80 intro. apply (witness (S O) n n). simplify.apply plus_n_O.
81 qed.
82
83 theorem divides_plus: \forall n,p,q:nat. 
84 n \divides p \to n \divides q \to n \divides p+q.
85 intros.
86 elim H.elim H1. apply (witness n (p+q) (n2+n1)).
87 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
88 qed.
89
90 theorem divides_minus: \forall n,p,q:nat. 
91 divides n p \to divides n q \to divides n (p-q).
92 intros.
93 elim H.elim H1. apply (witness n (p-q) (n2-n1)).
94 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
95 qed.
96
97 theorem divides_times: \forall n,m,p,q:nat. 
98 n \divides p \to m \divides q \to n*m \divides p*q.
99 intros.
100 elim H.elim H1. apply (witness (n*m) (p*q) (n2*n1)).
101 rewrite > H2.rewrite > H3.
102 apply (trans_eq nat ? (n*(m*(n2*n1)))).
103 apply (trans_eq nat ? (n*(n2*(m*n1)))).
104 apply assoc_times.
105 apply eq_f.
106 apply (trans_eq nat ? ((n2*m)*n1)).
107 apply sym_eq. apply assoc_times.
108 rewrite > (sym_times n2 m).apply assoc_times.
109 apply sym_eq. apply assoc_times.
110 qed.
111
112 theorem transitive_divides: transitive ? divides.
113 unfold.
114 intros.
115 elim H.elim H1. apply (witness x z (n2*n)).
116 rewrite > H3.rewrite > H2.
117 apply assoc_times.
118 qed.
119
120 variant trans_divides: \forall n,m,p. 
121  n \divides m \to m \divides p \to n \divides p \def transitive_divides.
122
123 theorem eq_mod_to_divides:\forall n,m,p. O< p \to
124 mod n p = mod m p \to divides p (n-m).
125 intros.
126 cut (n \le m \or \not n \le m).
127 elim Hcut.
128 cut (n-m=O).
129 rewrite > Hcut1.
130 apply (witness p O O).
131 apply times_n_O.
132 apply eq_minus_n_m_O.
133 assumption.
134 apply (witness p (n-m) ((div n p)-(div m p))).
135 rewrite > distr_times_minus.
136 rewrite > sym_times.
137 rewrite > (sym_times p).
138 cut ((div n p)*p = n - (mod n p)).
139 rewrite > Hcut1.
140 rewrite > eq_minus_minus_minus_plus.
141 rewrite > sym_plus.
142 rewrite > H1.
143 rewrite < div_mod.reflexivity.
144 assumption.
145 apply sym_eq.
146 apply plus_to_minus.
147 rewrite > sym_plus.
148 apply div_mod.
149 assumption.
150 apply (decidable_le n m).
151 qed.
152
153 theorem antisymmetric_divides: antisymmetric nat divides.
154 unfold antisymmetric.intros.elim H. elim H1.
155 apply (nat_case1 n2).intro.
156 rewrite > H3.rewrite > H2.rewrite > H4.
157 rewrite < times_n_O.reflexivity.
158 intros.
159 apply (nat_case1 n).intro.
160 rewrite > H2.rewrite > H3.rewrite > H5.
161 rewrite < times_n_O.reflexivity.
162 intros.
163 apply antisymmetric_le.
164 rewrite > H2.rewrite > times_n_SO in \vdash (? % ?).
165 apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n.
166 rewrite > H3.rewrite > times_n_SO in \vdash (? % ?).
167 apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n.
168 qed.
169
170 (* divides le *)
171 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
172 intros. elim H1.rewrite > H2.cut (O < n2).
173 apply (lt_O_n_elim n2 Hcut).intro.rewrite < sym_times.
174 simplify.rewrite < sym_plus.
175 apply le_plus_n.
176 elim (le_to_or_lt_eq O n2).
177 assumption.
178 absurd (O<m).assumption.
179 rewrite > H2.rewrite < H3.rewrite < times_n_O.
180 apply (not_le_Sn_n O).
181 apply le_O_n.
182 qed.
183
184 theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n.
185 intros.elim H1.
186 elim (le_to_or_lt_eq O n (le_O_n n)).
187 assumption.
188 rewrite < H3.absurd (O < m).assumption.
189 rewrite > H2.rewrite < H3.
190 simplify.exact (not_le_Sn_n O).
191 qed.
192
193 (* boolean divides *)
194 definition divides_b : nat \to nat \to bool \def
195 \lambda n,m :nat. (eqb (m \mod n) O).
196   
197 theorem divides_b_to_Prop :
198 \forall n,m:nat. O < n \to
199 match divides_b n m with
200 [ true \Rightarrow n \divides m
201 | false \Rightarrow n \ndivides m].
202 intros.unfold divides_b.
203 apply eqb_elim.
204 intro.simplify.apply mod_O_to_divides.assumption.assumption.
205 intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
206 qed.
207
208 theorem divides_b_true_to_divides :
209 \forall n,m:nat. O < n \to
210 (divides_b n m = true ) \to n \divides m.
211 intros.
212 change with 
213 match true with
214 [ true \Rightarrow n \divides m
215 | false \Rightarrow n \ndivides m].
216 rewrite < H1.apply divides_b_to_Prop.
217 assumption.
218 qed.
219
220 theorem divides_b_false_to_not_divides :
221 \forall n,m:nat. O < n \to
222 (divides_b n m = false ) \to n \ndivides m.
223 intros.
224 change with 
225 match false with
226 [ true \Rightarrow n \divides m
227 | false \Rightarrow n \ndivides m].
228 rewrite < H1.apply divides_b_to_Prop.
229 assumption.
230 qed.
231
232 theorem decidable_divides: \forall n,m:nat.O < n \to
233 decidable (n \divides m).
234 intros.unfold decidable.
235 cut 
236 (match divides_b n m with
237 [ true \Rightarrow n \divides m
238 | false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m).
239 apply Hcut.apply divides_b_to_Prop.assumption.
240 elim (divides_b n m).left.apply H1.right.apply H1.
241 qed.
242
243 theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
244 n \divides m \to divides_b n m = true.
245 intros.
246 cut (match (divides_b n m) with
247 [ true \Rightarrow n \divides m
248 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = true)).
249 apply Hcut.apply divides_b_to_Prop.assumption.
250 elim (divides_b n m).reflexivity.
251 absurd (n \divides m).assumption.assumption.
252 qed.
253
254 theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
255 \lnot(n \divides m) \to (divides_b n m) = false.
256 intros.
257 cut (match (divides_b n m) with
258 [ true \Rightarrow n \divides m
259 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = false)).
260 apply Hcut.apply divides_b_to_Prop.assumption.
261 elim (divides_b n m).
262 absurd (n \divides m).assumption.assumption.
263 reflexivity.
264 qed.
265
266 (* divides and pi *)
267 theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. 
268 m \le i \to i \le n+m \to f i \divides pi n f m.
269 intros 5.elim n.simplify.
270 cut (i = m).rewrite < Hcut.apply divides_n_n.
271 apply antisymmetric_le.assumption.assumption.
272 simplify.
273 cut (i < S n1+m \lor i = S n1 + m).
274 elim Hcut.
275 apply (transitive_divides ? (pi n1 f m)).
276 apply H1.apply le_S_S_to_le. assumption.
277 apply (witness ? ? (f (S n1+m))).apply sym_times.
278 rewrite > H3.
279 apply (witness ? ? (pi n1 f m)).reflexivity.
280 apply le_to_or_lt_eq.assumption.
281 qed.
282
283 (*
284 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. 
285 i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
286 intros.cut (pi n f) \mod (f i) = O.
287 rewrite < Hcut.
288 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
289 rewrite > Hcut.assumption.
290 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
291 apply divides_f_pi_f.assumption.
292 qed.
293 *)
294
295 (* divides and fact *)
296 theorem divides_fact : \forall n,i:nat. 
297 O < i \to i \le n \to i \divides n!.
298 intros 3.elim n.absurd (O<i).assumption.apply (le_n_O_elim i H1).
299 apply (not_le_Sn_O O).
300 change with (i \divides (S n1)*n1!).
301 apply (le_n_Sm_elim i n1 H2).
302 intro.
303 apply (transitive_divides ? n1!).
304 apply H1.apply le_S_S_to_le. assumption.
305 apply (witness ? ? (S n1)).apply sym_times.
306 intro.
307 rewrite > H3.
308 apply (witness ? ? n1!).reflexivity.
309 qed.
310
311 theorem mod_S_fact: \forall n,i:nat. 
312 (S O) < i \to i \le n \to (S n!) \mod i = (S O).
313 intros.cut (n! \mod i = O).
314 rewrite < Hcut.
315 apply mod_S.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
316 rewrite > Hcut.assumption.
317 apply divides_to_mod_O.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
318 apply divides_fact.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
319 assumption.
320 qed.
321
322 theorem not_divides_S_fact: \forall n,i:nat. 
323 (S O) < i \to i \le n \to i \ndivides S n!.
324 intros.
325 apply divides_b_false_to_not_divides.
326 apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
327 unfold divides_b.
328 rewrite > mod_S_fact.simplify.reflexivity.
329 assumption.assumption.
330 qed.
331
332 (* prime *)
333 definition prime : nat \to  Prop \def
334 \lambda n:nat. (S O) < n \land 
335 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
336
337 theorem not_prime_O: \lnot (prime O).
338 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
339 qed.
340
341 theorem not_prime_SO: \lnot (prime (S O)).
342 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
343 qed.
344
345 (* smallest factor *)
346 definition smallest_factor : nat \to nat \def
347 \lambda n:nat. 
348 match n with
349 [ O \Rightarrow O
350 | (S p) \Rightarrow 
351   match p with
352   [ O \Rightarrow (S O)
353   | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
354
355 (* it works ! 
356 theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
357 normalize.reflexivity.
358 qed.
359
360 theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)).
361 normalize.reflexivity.
362 qed.
363
364 theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
365 simplify.reflexivity.
366 qed. *)
367
368 theorem lt_SO_smallest_factor: 
369 \forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
370 intro.
371 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
372 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
373 intros.
374 change with 
375 (S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
376 apply (lt_to_le_to_lt ? (S (S O))).
377 apply (le_n (S(S O))).
378 cut ((S(S O)) = (S(S m1)) - m1).
379 rewrite > Hcut.
380 apply le_min_aux.
381 apply sym_eq.apply plus_to_minus.
382 rewrite < sym_plus.simplify.reflexivity.
383 qed.
384
385 theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
386 intro.
387 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
388 intro.apply (nat_case m).intro.
389 simplify.unfold lt.apply le_n.
390 intros.apply (trans_lt ? (S O)).
391 unfold lt.apply le_n.
392 apply lt_SO_smallest_factor.unfold lt. apply le_S_S.
393 apply le_S_S.apply le_O_n.
394 qed.
395
396 theorem divides_smallest_factor_n : 
397 \forall n:nat. O < n \to smallest_factor n \divides n.
398 intro.
399 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O O H).
400 intro.apply (nat_case m).intro. simplify.
401 apply (witness ? ? (S O)). simplify.reflexivity.
402 intros.
403 apply divides_b_true_to_divides.
404 apply (lt_O_smallest_factor ? H).
405 change with 
406 (eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) 
407   (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
408 apply f_min_aux_true.
409 apply (ex_intro nat ? (S(S m1))).
410 split.split.
411 apply le_minus_m.apply le_n.
412 rewrite > mod_n_n.reflexivity.
413 apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt.
414 apply le_S_S.apply le_S_S.apply le_O_n.
415 qed.
416   
417 theorem le_smallest_factor_n : 
418 \forall n:nat. smallest_factor n \le n.
419 intro.apply (nat_case n).simplify.apply le_n.
420 intro.apply (nat_case m).simplify.apply le_n.
421 intro.apply divides_to_le.
422 unfold lt.apply le_S_S.apply le_O_n.
423 apply divides_smallest_factor_n.
424 unfold lt.apply le_S_S.apply le_O_n.
425 qed.
426
427 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. 
428 (S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
429 intros 2.
430 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
431 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
432 intros.
433 apply divides_b_false_to_not_divides.
434 apply (trans_lt O (S O)).apply (le_n (S O)).assumption.unfold divides_b.
435 apply (lt_min_aux_to_false 
436 (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i).
437 cut ((S(S O)) = (S(S m1)-m1)).
438 rewrite < Hcut.exact H1.
439 apply sym_eq. apply plus_to_minus.
440 rewrite < sym_plus.simplify.reflexivity.
441 exact H2.
442 qed.
443
444 theorem prime_smallest_factor_n : 
445 \forall n:nat. (S O) < n \to prime (smallest_factor n).
446 intro.change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land 
447 (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to  m = (smallest_factor n))).
448 intro.split.
449 apply lt_SO_smallest_factor.assumption.
450 intros.
451 cut (le m (smallest_factor n)).
452 elim (le_to_or_lt_eq m (smallest_factor n) Hcut).
453 absurd (m \divides n).
454 apply (transitive_divides m (smallest_factor n)).
455 assumption.
456 apply divides_smallest_factor_n.
457 apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H.
458 apply lt_smallest_factor_to_not_divides.
459 exact H.assumption.assumption.assumption.
460 apply divides_to_le.
461 apply (trans_lt O (S O)).
462 apply (le_n (S O)).
463 apply lt_SO_smallest_factor.
464 exact H.
465 assumption.
466 qed.
467
468 theorem prime_to_smallest_factor: \forall n. prime n \to
469 smallest_factor n = n.
470 intro.apply (nat_case n).intro.apply False_ind.apply (not_prime_O H).
471 intro.apply (nat_case m).intro.apply False_ind.apply (not_prime_SO H).
472 intro.
473 change with 
474 ((S O) < (S(S m1)) \land 
475 (\forall m:nat. m \divides S(S m1) \to (S O) < m \to  m = (S(S m1))) \to 
476 smallest_factor (S(S m1)) = (S(S m1))).
477 intro.elim H.apply H2.
478 apply divides_smallest_factor_n.
479 apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption.
480 apply lt_SO_smallest_factor.
481 assumption.
482 qed.
483
484 (* a number n > O is prime iff its smallest factor is n *)
485 definition primeb \def \lambda n:nat.
486 match n with
487 [ O \Rightarrow false
488 | (S p) \Rightarrow
489   match p with
490   [ O \Rightarrow false
491   | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]].
492
493 (* it works! 
494 theorem example4 : primeb (S(S(S O))) = true.
495 normalize.reflexivity.
496 qed.
497
498 theorem example5 : primeb (S(S(S(S(S(S O)))))) = false.
499 normalize.reflexivity.
500 qed.
501
502 theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true.
503 normalize.reflexivity.
504 qed.
505
506 theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true.
507 normalize.reflexivity.
508 qed. *)
509
510 theorem primeb_to_Prop: \forall n.
511 match primeb n with
512 [ true \Rightarrow prime n
513 | false \Rightarrow \lnot (prime n)].
514 intro.
515 apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
516 intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
517 intro.
518 change with 
519 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
520 [ true \Rightarrow prime (S(S m1))
521 | false \Rightarrow \lnot (prime (S(S m1)))].
522 apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
523 intro.simplify.
524 rewrite < H.
525 apply prime_smallest_factor_n.
526 unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.
527 intro.simplify.
528 change with (prime (S(S m1)) \to False).
529 intro.apply H.
530 apply prime_to_smallest_factor.
531 assumption.
532 qed.
533
534 theorem primeb_true_to_prime : \forall n:nat.
535 primeb n = true \to prime n.
536 intros.change with
537 match true with 
538 [ true \Rightarrow prime n
539 | false \Rightarrow \lnot (prime n)].
540 rewrite < H.
541 apply primeb_to_Prop.
542 qed.
543
544 theorem primeb_false_to_not_prime : \forall n:nat.
545 primeb n = false \to \lnot (prime n).
546 intros.change with
547 match false with 
548 [ true \Rightarrow prime n
549 | false \Rightarrow \lnot (prime n)].
550 rewrite < H.
551 apply primeb_to_Prop.
552 qed.
553
554 theorem decidable_prime : \forall n:nat.decidable (prime n).
555 intro.unfold decidable.
556 cut 
557 (match primeb n with
558 [ true \Rightarrow prime n
559 | false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n)).
560 apply Hcut.apply primeb_to_Prop.
561 elim (primeb n).left.apply H.right.apply H.
562 qed.
563
564 theorem prime_to_primeb_true: \forall n:nat. 
565 prime n \to primeb n = true.
566 intros.
567 cut (match (primeb n) with
568 [ true \Rightarrow prime n
569 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = true)).
570 apply Hcut.apply primeb_to_Prop.
571 elim (primeb n).reflexivity.
572 absurd (prime n).assumption.assumption.
573 qed.
574
575 theorem not_prime_to_primeb_false: \forall n:nat. 
576 \lnot(prime n) \to primeb n = false.
577 intros.
578 cut (match (primeb n) with
579 [ true \Rightarrow prime n
580 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = false)).
581 apply Hcut.apply primeb_to_Prop.
582 elim (primeb n).
583 absurd (prime n).assumption.assumption.
584 reflexivity.
585 qed.
586