More notation here and there.

[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 ca9eac304b2538954a953bdf85d09bbac7e8907e..83c98b68380f2fe7edc3fa0db124a176b35cd0d8 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 \lnot (mod n m = O) \to
+theorem plog_exp: \forall n,m,i. O < m \to mod n m \neq 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.
@@ -150,7 +150,7 @@ qed.
 
 theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
   match plog_aux p n m with
-  [ (pair q r) \Rightarrow \lnot (mod r m = O)].
+  [ (pair q r) \Rightarrow mod r m \neq O].
 intro.elim p.absurd O < n.assumption.
 apply le_to_not_lt.assumption.
 change with
@@ -161,7 +161,7 @@ match
         [ (pair q r) \Rightarrow pair nat nat (S q) r]
     | (S a) \Rightarrow pair nat nat O n1])
 with
-  [ (pair q r) \Rightarrow \lnot(mod r m = O)].
+  [ (pair q r) \Rightarrow mod r m \neq O].
 apply nat_case1 (mod n1 m).intro.
 generalize in match (H (div n1 m) m).
 elim (plog_aux n (div n1 m) m).
@@ -173,7 +173,7 @@ apply le_S_S_to_le.
 apply trans_le ? n1.change with div n1 m < n1.
 apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
-change with (\lnot (mod n1 m = O)).
+change with mod n1 m \neq O.
 rewrite > H4.
 (* Andrea: META NOT FOUND !!!  
 rewrite > sym_eq. *)
@@ -183,11 +183,11 @@ rewrite > H5.reflexivity.
 qed.
 
 theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
- pair nat nat q r = plog_aux p n m \to \lnot (mod r m = O).
+ pair nat nat q r = plog_aux p n m \to mod r m \neq O.
 intros.
 change with 
   match (pair nat nat q r) with
-  [ (pair q r) \Rightarrow \lnot (mod r m = O)].
+  [ (pair q r) \Rightarrow mod r m \neq O].
 rewrite > H3. 
 apply plog_aux_to_Prop1.
 assumption.assumption.assumption.