More notation here and there.

[helm.git] / helm / matita / library / Q / q.ma

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index f04603f15f0b129423e8bd5a0fe289f2495b7cbc..6e3639f6e726b27ad9dfb37b0004c8abbaa18748 100644 (file)
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -117,7 +117,7 @@ change with (ftl (cons x f)) = (ftl (cons y g)).
 apply eq_f.assumption.
 qed.
 
-theorem not_eq_pp_nn: \forall n,m:nat. \lnot (pp n) = (nn m).
+theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
 intros.simplify. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
@@ -129,7 +129,7 @@ qed.
 
 theorem not_eq_pp_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
-\lnot (pp n) = (cons x f).
+pp n \neq cons x f.
 intros.simplify. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
@@ -141,7 +141,7 @@ qed.
 
 theorem not_eq_nn_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
-\lnot (nn n) = (cons x f).
+nn n \neq cons x f.
 intros.simplify. intro.
 change with match (nn n) with
 [ (pp n) \Rightarrow True
@@ -180,11 +180,11 @@ qed.
 theorem eqfb_to_Prop: \forall f,g:fraction.
 match (eqfb f g) with
 [true \Rightarrow f=g
-|false \Rightarrow \lnot f=g].
+|false \Rightarrow f \neq g].
 intros.apply fraction_elim2 
 (\lambda f,g.match (eqfb f g) with
 [true \Rightarrow f=g
-|false \Rightarrow \lnot f=g]).
+|false \Rightarrow f \neq g]).
   intros.elim g1.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.