More notation here and there.

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

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index e20d824df5ae105129599fda2b93beac3a23fcfb..ba3151a3b34ce7da6f27148ab193d50abe6680b5 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -32,12 +32,12 @@ match n with
 theorem eqb_to_Prop: \forall n,m:nat. 
 match (eqb n m) with
 [ true  \Rightarrow n = m 
-| false \Rightarrow \lnot (n = m)].
+| false \Rightarrow n \neq m].
 intros.
 apply nat_elim2
 (\lambda n,m:nat.match (eqb n m) with
 [ true  \Rightarrow n = m 
-| false \Rightarrow \lnot (n = m)]).
+| false \Rightarrow n \neq m]).
 intro.elim n1.
 simplify.reflexivity.
 simplify.apply not_eq_O_S.
@@ -52,12 +52,12 @@ simplify.intro.apply H1.apply inj_S.assumption.
 qed.
 
 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
-(n=m \to (P true)) \to (\lnot n=m \to (P false)) \to (P (eqb n m)). 
+(n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)). 
 intros.
 cut 
 match (eqb n m) with
 [ true  \Rightarrow n = m
-| false \Rightarrow \lnot (n = m)] \to (P (eqb n m)).
+| false \Rightarrow n \neq m] \to (P (eqb n m)).
 apply Hcut.apply eqb_to_Prop.
 elim eqb n m.
 apply (H H2).
@@ -75,12 +75,12 @@ match n with
 theorem leb_to_Prop: \forall n,m:nat. 
 match (leb n m) with
 [ true  \Rightarrow n \leq m 
-| false \Rightarrow \lnot (n \leq m)].
+| false \Rightarrow n \nleq m].
 intros.
 apply nat_elim2
 (\lambda n,m:nat.match (leb n m) with
 [ true  \Rightarrow n \leq m 
-| false \Rightarrow \lnot (n \leq m)]).
+| false \Rightarrow n \nleq m]).
 simplify.exact le_O_n.
 simplify.exact not_le_Sn_O.
 intros 2.simplify.elim (leb n1 m1).
@@ -89,13 +89,13 @@ simplify.intros.apply H.apply le_S_S_to_le.assumption.
 qed.
 
 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
-(n \leq m \to (P true)) \to (\lnot (n \leq m) \to (P false)) \to
+(n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
 P (leb n m).
 intros.
 cut 
 match (leb n m) with
 [ true  \Rightarrow n \leq m
-| false \Rightarrow \lnot (n \leq m)] \to (P (leb n m)).
+| false \Rightarrow n \nleq m] \to (P (leb n m)).
 apply Hcut.apply leb_to_Prop.
 elim leb n m.
 apply (H H2).