More notation here and there.

[helm.git] / helm / matita / library / nat / factorization.ma

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index 1b946be522c143b6be9e1082dab079c9b82a86dd..c9669e2ba0a8071e58cf3e07a407f8d9e77b9478 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -87,7 +87,7 @@ apply divides_max_prime_factor_n.
 assumption.
 change with nth_prime (max_prime_factor n) \divides r \to False.
 intro.
-cut \lnot (mod r (nth_prime (max_prime_factor n))) = O.
+cut mod r (nth_prime (max_prime_factor n)) \neq O.
 apply Hcut1.apply divides_to_mod_O.
 apply lt_O_nth_prime_n.assumption.
 apply plog_aux_to_not_mod_O n n ? q r.
@@ -195,7 +195,7 @@ rewrite > Hcut.rewrite < H4.reflexivity.
 simplify. intro.apply not_le_Sn_O O.
 rewrite < H5 in \vdash (? ? %).assumption.
 apply le_to_or_lt_eq.apply le_O_n.
-cut (S O) < r \lor \lnot (S O) < r.
+cut (S O) < r \lor (S O) \nlt r.
 elim Hcut1.
 right.
 apply plog_to_lt_max_prime_factor1 n1 ? q r.
@@ -285,7 +285,7 @@ rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
 assumption.
 apply le_to_or_lt_eq.apply le_O_n.assumption.
 (* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
-cut (S O) < r \lor \lnot (S O) < r.
+cut (S O) < r \lor S O \nlt r.
 elim Hcut2.
 right. 
 apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r.