More notation here and there: \sup, \divides, \ndivides, !

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

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index e7fd12f15836693f941cfcd3696b2ff598cbb81e..ca9eac304b2538954a953bdf85d09bbac7e8907e 100644 (file)
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -89,7 +89,7 @@ apply plog_aux_to_Prop.
 assumption.
 qed.
 (* questo va spostato in primes1.ma *)
-theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to
+theorem plog_exp: \forall n,m,i. O < m \to \lnot (mod n m = O) \to
 \forall p. i \le p \to plog_aux p (m \sup i * n) m = pair nat nat i n.
 intros 5.
 elim i.