(cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
theorem reflexive_divides : reflexive nat divides.
-simplify.
+unfold reflexive.
intros.
exact (witness x x (S O) (times_n_SO x)).
qed.
apply (decidable_le n m).
qed.
+theorem antisymmetric_divides: antisymmetric nat divides.
+unfold antisymmetric.intros.elim H. elim H1.
+apply (nat_case1 n2).intro.
+rewrite > H3.rewrite > H2.rewrite > H4.
+rewrite < times_n_O.reflexivity.
+intros.
+apply (nat_case1 n).intro.
+rewrite > H2.rewrite > H3.rewrite > H5.
+rewrite < times_n_O.reflexivity.
+intros.
+apply antisymmetric_le.
+rewrite > H2.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n.
+rewrite > H3.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n.
+qed.
+
(* divides le *)
theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
intros. elim H1.rewrite > H2.cut (O < n2).
| false \Rightarrow n \ndivides m].
apply eqb_elim.
intro.simplify.apply mod_O_to_divides.assumption.assumption.
-intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
+intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
qed.
theorem divides_b_true_to_divides :
(\forall m:nat. m \divides n \to (S O) < m \to m = n).
theorem not_prime_O: \lnot (prime O).
-simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
qed.
theorem not_prime_SO: \lnot (prime (S O)).
-simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
qed.
(* smallest factor *)
intro.
apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
intro.apply (nat_case m).intro.
-simplify.apply le_n.
+simplify.unfold lt.apply le_n.
intros.apply (trans_lt ? (S O)).
-simplify. apply le_n.
-apply lt_SO_smallest_factor.simplify. apply le_S_S.
+unfold lt.apply le_n.
+apply lt_SO_smallest_factor.unfold lt. apply le_S_S.
apply le_S_S.apply le_O_n.
qed.
split.split.
apply le_minus_m.apply le_n.
rewrite > mod_n_n.reflexivity.
-apply (trans_lt ? (S O)).apply (le_n (S O)).simplify.
+apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt.
apply le_S_S.apply le_S_S.apply le_O_n.
qed.
intro.apply (nat_case n).simplify.reflexivity.
intro.apply (nat_case m).simplify.reflexivity.
intro.apply divides_to_le.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
qed.
theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
apply (transitive_divides m (smallest_factor n)).
assumption.
apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. exact H.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H.
apply lt_smallest_factor_to_not_divides.
exact H.assumption.assumption.assumption.
apply divides_to_le.
smallest_factor (S(S m1)) = (S(S m1))).
intro.elim H.apply H2.
apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)).simplify. apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption.
apply lt_SO_smallest_factor.
assumption.
qed.
[ true \Rightarrow prime n
| false \Rightarrow \lnot (prime n)].
intro.
-apply (nat_case n).simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
-intro.apply (nat_case m).simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
+intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
intro.
change with
match eqb (smallest_factor (S(S m1))) (S(S m1)) with
intro.change with (prime (S(S m1))).
rewrite < H.
apply prime_smallest_factor_n.
-simplify.apply le_S_S.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.
intro.change with (\lnot (prime (S(S m1)))).
change with (prime (S(S m1)) \to False).
intro.apply H.