From 73e63e535940a068e660d3688a3c8ebfa1930561 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 22 Sep 2005 17:40:42 +0000
Subject: [PATCH] More notation here and there.

---
 helm/matita/library/Q/q.ma               | 10 +++++-----
 helm/matita/library/Z/compare.ma         |  6 +++---
 helm/matita/library/Z/z.ma               |  8 ++++----
 helm/matita/library/datatypes/bool.ma    |  2 +-
 helm/matita/library/nat/compare.ma       | 16 ++++++++--------
 helm/matita/library/nat/div_and_mod.ma   |  2 +-
 helm/matita/library/nat/factorization.ma |  6 +++---
 helm/matita/library/nat/log.ma           | 12 ++++++------
 helm/matita/library/nat/lt_arith.ma      |  2 +-
 helm/matita/library/nat/minus.ma         |  2 +-
 helm/matita/library/nat/nat.ma           |  6 +++---
 helm/matita/library/nat/orders.ma        | 12 ++++++------
 12 files changed, 42 insertions(+), 42 deletions(-)

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index f04603f15..6e3639f6e 100644
--- 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.
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).
diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 423399ff2..8ce0047e1 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -51,7 +51,7 @@ match z with
 theorem OZ_test_to_Prop :\forall z:Z.
 match OZ_test z with
 [true \Rightarrow z=OZ 
-|false \Rightarrow \lnot (z=OZ)].
+|false \Rightarrow z \neq OZ].
 intros.elim z.
 simplify.reflexivity.
 simplify.intros [H].
@@ -81,17 +81,17 @@ qed.
 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
 \def injective_neg.
 
-theorem not_eq_OZ_pos: \forall n:nat. \lnot (OZ = (pos n)).
+theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
 simplify.intros [n; H].
 discriminate H.
 qed.
 
-theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)).
+theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
 simplify.intros [n; H].
 discriminate H.
 qed.
 
-theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)).
+theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
 simplify.intros [n; m; H].
 discriminate H.
 qed.
diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index d99456dc8..a223d7d0c 100644
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -20,7 +20,7 @@ inductive bool : Set \def
   | true : bool
   | false : bool.
   
-theorem not_eq_true_false : \lnot true = false.
+theorem not_eq_true_false : true \neq false.
 simplify.intro.
 change with 
 match true with
diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index e20d824df..ba3151a3b 100644
--- 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).
diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 73344c7c4..af5ee9808 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -101,7 +101,7 @@ definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
 \lambda n,m,q,r:nat.r < m \land n=q*m+r).
 *)
 
-theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to \lnot m=O.
+theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
 intros 4.simplify.intros.elim H.absurd le (S r) O.
 rewrite < H1.assumption.
 exact not_le_Sn_O r.
diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index 1b946be52..c9669e2ba 100644
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -87,7 +87,7 @@ apply divides_max_prime_factor_n.
 assumption.
 change with nth_prime (max_prime_factor n) \divides r \to False.
 intro.
-cut \lnot (mod r (nth_prime (max_prime_factor n))) = O.
+cut mod r (nth_prime (max_prime_factor n)) \neq O.
 apply Hcut1.apply divides_to_mod_O.
 apply lt_O_nth_prime_n.assumption.
 apply plog_aux_to_not_mod_O n n ? q r.
@@ -195,7 +195,7 @@ rewrite > Hcut.rewrite < H4.reflexivity.
 simplify. intro.apply not_le_Sn_O O.
 rewrite < H5 in \vdash (? ? %).assumption.
 apply le_to_or_lt_eq.apply le_O_n.
-cut (S O) < r \lor \lnot (S O) < r.
+cut (S O) < r \lor (S O) \nlt r.
 elim Hcut1.
 right.
 apply plog_to_lt_max_prime_factor1 n1 ? q r.
@@ -285,7 +285,7 @@ rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
 assumption.
 apply le_to_or_lt_eq.apply le_O_n.assumption.
 (* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
-cut (S O) < r \lor \lnot (S O) < r.
+cut (S O) < r \lor S O \nlt r.
 elim Hcut2.
 right. 
 apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r.
diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index ca9eac304..83c98b683 100644
--- 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.
diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 19f25a967..a2e7f6109 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -116,7 +116,7 @@ qed.
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 intros.
-cut p < q \lor \lnot (p < q).
+cut p < q \lor p \nlt q.
 elim Hcut.
 assumption.
 absurd p * (S n) < q * (S n).
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index cbf92049c..3b39ed43f 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -235,7 +235,7 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 
 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 intros.
-cut m+p \le n \or \lnot m+p \le n.
+cut m+p \le n \or m+p \nleq n.
   elim Hcut.
     symmetry.apply plus_to_minus.assumption.
     rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index aae6434e7..e2bf56542 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -41,7 +41,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. 
-\lnot n=m \to \lnot (S n = S m).
+\lnot n=m \to S n \neq S m.
 intros. simplify. intros.
 apply H. apply injective_S. assumption.
 qed.
@@ -52,14 +52,14 @@ definition not_zero : nat \to Prop \def
   [ O \Rightarrow False
   | (S p) \Rightarrow True ].
 
-theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
+theorem not_eq_O_S : \forall n:nat. O \neq S n.
 intros. simplify. intros.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
 qed.
 
-theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
+theorem not_eq_n_Sn : \forall n:nat. n \neq S n.
 intros.elim n.
 apply not_eq_O_S.
 apply not_eq_S.assumption.
diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 71cd59450..796567fa5 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -104,11 +104,11 @@ intros.elim H.exact I.exact I.
 qed.
 
 (* not le *)
-theorem not_le_Sn_O: \forall n:nat. \lnot (S n \leq O).
+theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
 intros.simplify.intros.apply leS_to_not_zero ? ? H.
 qed.
 
-theorem not_le_Sn_n: \forall n:nat. \lnot (S n \leq n).
+theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
 intros.elim n.apply not_le_Sn_O.simplify.intros.cut S n1 \leq n1.
 apply H.assumption.
 apply le_S_S_to_le.assumption.
@@ -123,7 +123,7 @@ left.simplify.apply le_S_S.assumption.
 qed.
 
 (* not eq *)
-theorem lt_to_not_eq : \forall n,m:nat. n<m \to \lnot (n=m).
+theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
 simplify.intros.cut (le (S n) m) \to False.
 apply Hcut.assumption.rewrite < H1.
 apply not_le_Sn_n.
@@ -141,16 +141,16 @@ simplify.intros.
 apply le_S_S_to_le.assumption.
 qed.
 
-theorem not_le_to_lt: \forall n,m:nat. \lnot (n \leq m) \to m<n.
+theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
 intros 2.
-apply nat_elim2 (\lambda n,m.\lnot (n \leq m) \to m<n).
+apply nat_elim2 (\lambda n,m.n \nleq m \to m<n).
 intros.apply absurd (O \leq n1).apply le_O_n.assumption.
 simplify.intros.apply le_S_S.apply le_O_n.
 simplify.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
 assumption.
 qed.
 
-theorem lt_to_not_le: \forall n,m:nat. n<m \to \lnot (m \leq n).
+theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
 simplify.intros 3.elim H.
 apply not_le_Sn_n n H1.
 apply H2.apply lt_to_le. apply H3.
-- 
2.39.2