X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Fcompare.ma;h=1bf4f066abe593fc886dab62f61b3a48f342101e;hb=73e63e535940a068e660d3688a3c8ebfa1930561;hp=3b259b4f664b0b19d1d8ec646596600e135e693e;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index 3b259b4f6..1bf4f066a 100644
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -41,7 +41,7 @@ theorem eqZb_to_Prop:
 \forall x,y:Z. 
 match eqZb x y with
 [ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y].
+| false \Rightarrow x \neq y].
 intros.
 elim x.
   elim y.
@@ -63,12 +63,12 @@ elim x.
 qed.
 
 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
-(x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
+(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
 intros.
 cut 
 match (eqZb x y) with
 [ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y] \to P (eqZb x y).
+| false \Rightarrow x \neq y] \to P (eqZb x y).
 apply Hcut.
 apply eqZb_to_Prop.
 elim (eqZb).