X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnat.ma;h=194cf1273b4eb5c7719be019376a02cab8016f3c;hb=3224a2614b5734dd9c32e17049253a9427507c4f;hp=100a101f95e1fa27797ea2e92e1be7eb456a578b;hpb=633474751ddf1074947ff0d324fb1aca2293eff8;p=helm.git

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index 100a101f9..194cf1273 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -43,7 +43,7 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
 \def injective_S.
 
 theorem not_eq_S  : \forall n,m:nat. 
-Not (n=m) \to Not (S n = S m).
+\lnot n=m \to \lnot (S n = S m).
 intros. simplify. intros.
 apply H. apply injective_S. assumption.
 qed.
@@ -54,14 +54,14 @@ definition not_zero : nat \to Prop \def
   [ O \Rightarrow False
   | (S p) \Rightarrow True ].
 
-theorem not_eq_O_S : \forall n:nat. Not (O=S n).
+theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
 intros. simplify. intros.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
 qed.
 
-theorem not_eq_n_Sn : \forall n:nat. Not (n=S n).
+theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
 intros.elim n.
 apply not_eq_O_S.
 apply not_eq_S.assumption.