From 3eff4cc36820df9faddb3cb16390717851db499c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 25 Jul 2005 21:10:16 +0000
Subject: [PATCH] A little bit more of notation here and there.

---
 helm/matita/library/Z/z.ma                    |  2 +-
 helm/matita/library/datatypes/bool.ma         |  8 +++
 .../library/higher_order_defs/relations.ma    |  2 +-
 helm/matita/library/logic/connectives.ma      | 17 +++--
 helm/matita/library/logic/equality.ma         |  4 +-
 helm/matita/library/nat/compare.ma            | 28 ++++----
 helm/matita/library/nat/div_and_mod.ma        | 48 +++++++-------
 helm/matita/library/nat/minus.ma              | 54 ++++++++-------
 helm/matita/library/nat/nat.ma                |  6 +-
 helm/matita/library/nat/orders.ma             | 65 +++++++++++--------
 helm/matita/library/nat/orders_op.ma          | 37 +++++------
 helm/matita/library/nat/plus.ma               | 19 +++---
 helm/matita/library/nat/times.ma              | 17 ++---
 13 files changed, 166 insertions(+), 141 deletions(-)

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 5aa5d9083..9dffcee52 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -52,7 +52,7 @@ match z with
 theorem OZ_test_to_Prop :\forall z:Z.
 match OZ_test z with
 [true \Rightarrow eq Z z OZ 
-|false \Rightarrow Not (eq Z z OZ)].
+|false \Rightarrow \lnot (eq Z z OZ)].
 intros.elim z.
 simplify.reflexivity.
 simplify.intros.
diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index fdb376c60..8267aa7f6 100644
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -24,6 +24,8 @@ definition notb : bool \to bool \def
  [ true \Rightarrow false
  | false \Rightarrow true ].
 
+interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x).
+
 definition andb : bool \to bool \to bool\def
 \lambda b1,b2:bool. 
  match b1 with 
@@ -31,6 +33,8 @@ definition andb : bool \to bool \to bool\def
 	match b2 with [true \Rightarrow true | false \Rightarrow false]
  | false \Rightarrow false ].
 
+interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y).
+
 definition orb : bool \to bool \to bool\def
 \lambda b1,b2:bool. 
  match b1 with 
@@ -38,8 +42,12 @@ definition orb : bool \to bool \to bool\def
 	match b2 with [true \Rightarrow true | false \Rightarrow false]
  | false \Rightarrow false ].
 
+interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y).
+
 definition if_then_else : bool \to Prop \to Prop \to Prop \def 
 \lambda b:bool.\lambda P,Q:Prop.
 match b with
 [ true \Rightarrow P
 | false  \Rightarrow Q].
+
+(*CSC: missing notation for if_then_else *)
diff --git a/helm/matita/library/higher_order_defs/relations.ma b/helm/matita/library/higher_order_defs/relations.ma
index a2aa625a7..029b229dc 100644
--- a/helm/matita/library/higher_order_defs/relations.ma
+++ b/helm/matita/library/higher_order_defs/relations.ma
@@ -30,4 +30,4 @@ definition transitive: \forall A:Type.\forall R:A \to A \to Prop.Prop
 
 definition irreflexive: \forall A:Type.\forall R:A \to A \to Prop.Prop
 \def 
-\lambda A.\lambda R.\forall x:A.Not (R x x).
\ No newline at end of file
+\lambda A.\lambda R.\forall x:A.\lnot (R x x).
diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index a5aab65f5..5a1ad1fdd 100644
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -26,7 +26,10 @@ default "false" cic:/matita/logic/connectives/False.ind.
 definition Not: Prop \to Prop \def
 \lambda A. (A \to False).
 
-theorem absurd : \forall A,C:Prop. A \to Not A \to C.
+interpretation "logical not" 'not x = (cic:/matita/logic/connectives/Not.con x).
+alias symbol "not" (instance 0) = "logical not".
+
+theorem absurd : \forall A,C:Prop. A \to \lnot A \to C.
 intros. elim (H1 H).
 qed.
 
@@ -35,19 +38,25 @@ default "absurd" cic:/matita/logic/connectives/absurd.con.
 inductive And (A,B:Prop) : Prop \def
     conj : A \to B \to (And A B).
 
-theorem proj1: \forall A,B:Prop. (And A B) \to A.
+interpretation "logical and" 'and x y = (cic:/matita/logic/connectives/And.ind#xpointer(1/1) x y).
+alias symbol "and" (instance 0) = "logical and".
+
+theorem proj1: \forall A,B:Prop. A \land B \to A.
 intros. elim H. assumption.
 qed.
 
-theorem proj2: \forall A,B:Prop. (And A B) \to B.
+theorem proj2: \forall A,B:Prop. A \land B \to B.
 intros. elim H. assumption.
 qed.
 
 inductive Or (A,B:Prop) : Prop \def
      or_introl : A \to (Or A B)
    | or_intror : B \to (Or A B).
+
+interpretation "logical or" 'or x y = (cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y).
+alias symbol "or" (instance 0) = "logical or".
    
-definition decidable : Prop \to Prop \def \lambda A:Prop. Or A (Not A).
+definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A.
 
 inductive ex (A:Type) (P:A \to Prop) : Prop \def
     ex_intro: \forall x:A. P x \to ex A P.
diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 0be69f9b7..87fe22bac 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -56,12 +56,12 @@ default "equality"
  cic:/matita/logic/equality/eq_elim_r.con. 
  
 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
-\forall x,y:A. x=y \to (f x)=(f y).
+\forall x,y:A. x=y \to f x = f y.
 intros.elim H.reflexivity.
 qed.
 
 theorem eq_f2: \forall  A,B,C:Type.\forall f:A\to B \to C.
 \forall x1,x2:A. \forall y1,y2:B.
-x1=x2 \to y1=y2 \to (f x1 y1)=(f x2 y2).
+x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
 intros.elim H1.elim H.reflexivity.
 qed.
diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 16d689e4c..60a9d4194 100644
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -28,13 +28,13 @@ match n with
 	
 theorem leb_to_Prop: \forall n,m:nat. 
 match (leb n m) with
-[ true  \Rightarrow (le n m) 
-| false \Rightarrow (Not (le n m))].
+[ true  \Rightarrow n \leq m 
+| false \Rightarrow \lnot (n \leq m)].
 intros.
 apply nat_elim2
 (\lambda n,m:nat.match (leb n m) with
-[ true  \Rightarrow (le n m) 
-| false \Rightarrow (Not (le n m))]).
+[ true  \Rightarrow n \leq m 
+| false \Rightarrow \lnot (n \leq m)]).
 simplify.exact le_O_n.
 simplify.exact not_le_Sn_O.
 intros 2.simplify.elim (leb n1 m1).
@@ -43,13 +43,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. 
-((le n m) \to (P true)) \to ((Not (le n m)) \to (P false)) \to
+(n \leq m \to (P true)) \to (\not (n \leq m) \to (P false)) \to
 P (leb n m).
 intros.
 cut 
 match (leb n m) with
-[ true  \Rightarrow (le n m) 
-| false \Rightarrow (Not (le n m))] \to (P (leb n m)).
+[ true  \Rightarrow n \leq m
+| false \Rightarrow \lnot (n \leq m)] \to (P (leb n m)).
 apply Hcut.apply leb_to_Prop.
 elim leb n m.
 apply (H H2).
@@ -80,14 +80,14 @@ qed.
 
 theorem nat_compare_to_Prop: \forall n,m:nat. 
 match (nat_compare n m) with
-  [ LT \Rightarrow (lt n m)
+  [ LT \Rightarrow n < m
   | EQ \Rightarrow n=m
-  | GT \Rightarrow (lt m n) ].
+  | GT \Rightarrow m < n ].
 intros.
 apply nat_elim2 (\lambda n,m.match (nat_compare n m) with
-  [ LT \Rightarrow (lt n m)
+  [ LT \Rightarrow n < m
   | EQ \Rightarrow n=m
-  | GT \Rightarrow (lt m n) ]).
+  | GT \Rightarrow m < n ]).
 intro.elim n1.simplify.reflexivity.
 simplify.apply le_S_S.apply le_O_n.
 intro.simplify.apply le_S_S. apply le_O_n.
@@ -109,13 +109,13 @@ intros.simplify.elim H.reflexivity.
 qed.
      
 theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
-((lt n m) \to (P LT)) \to (n=m \to (P EQ)) \to ((lt m n) \to (P GT)) \to 
+(n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to 
 (P (nat_compare n m)).
 intros.
 cut match (nat_compare n m) with
-[ LT \Rightarrow (lt n m)
+[ LT \Rightarrow n < m
 | EQ \Rightarrow n=m
-| GT \Rightarrow (lt m n)] \to
+| GT \Rightarrow m < n] \to
 (P (nat_compare n m)).
 apply Hcut.apply nat_compare_to_Prop.
 elim (nat_compare n m).
diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 4c43d33bd..ca8b6c3fa 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -24,7 +24,7 @@ match (leb m n) with
 | false \Rightarrow
   match p with
   [O \Rightarrow m
-  |(S q) \Rightarrow mod_aux q (minus m (S n)) n]].
+  |(S q) \Rightarrow mod_aux q (m-(S n)) n]].
 
 definition mod : nat \to nat \to nat \def
 \lambda n,m.
@@ -38,7 +38,7 @@ match (leb m n) with
 | false \Rightarrow
   match p with
   [O \Rightarrow O
-  |(S q) \Rightarrow S (div_aux q (minus m (S n)) n)]].
+  |(S q) \Rightarrow S (div_aux q (m-(S n)) n)]].
 
 definition div : nat \to nat \to nat \def
 \lambda n,m.
@@ -47,15 +47,15 @@ match m with
 | (S p) \Rightarrow div_aux n n p]. 
 
 theorem le_mod_aux_m_m: 
-\forall p,n,m. (le n p) \to (le (mod_aux p n m) m).
+\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
 intro.elim p.
-apply le_n_O_elim n H (\lambda n.(le (mod_aux O n m) m)).
+apply le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m).
 simplify.apply le_O_n.
 simplify.
 apply leb_elim n1 m.
 simplify.intro.assumption.
 simplify.intro.apply H.
-cut (le n1 (S n)) \to (le (minus n1 (S m)) n).
+cut n1 \leq (S n) \to n1-(S m) \leq n.
 apply Hcut.assumption.
 elim n1.
 simplify.apply le_O_n.
@@ -63,7 +63,7 @@ simplify.apply trans_le ? n2 n.
 apply le_minus_m.apply le_S_S_to_le.assumption.
 qed.
 
-theorem lt_mod_m_m: \forall n,m. (lt O m) \to (lt (mod n m) m).
+theorem lt_mod_m_m: \forall n,m. O < m \to (mod n m) < m.
 intros 2.elim m.apply False_ind.
 apply not_le_Sn_O O H.
 simplify.apply le_S_S.apply le_mod_aux_m_m.
@@ -71,7 +71,7 @@ apply le_n.
 qed.
 
 theorem div_aux_mod_aux: \forall p,n,m:nat. 
-(n=plus (times (div_aux p n m) (S m)) (mod_aux p n m)).
+(n=(div_aux p n m)*(S m) + (mod_aux p n m)).
 intro.elim p.
 simplify.elim leb n m.
 simplify.apply refl_eq.
@@ -81,38 +81,36 @@ apply leb_elim n1 m.
 simplify.intro.apply refl_eq.
 simplify.intro.
 rewrite > assoc_plus. 
-elim (H (minus n1 (S m)) m).
-change with (n1=plus (S m) (minus n1 (S m))).
+elim (H (n1-(S m)) m).
+change with (n1=(S m)+(n1-(S m))).
 rewrite < sym_plus.
 apply plus_minus_m_m.
-change with lt m n1.
+change with m < n1.
 apply not_le_to_lt.exact H1.
 qed.
 
-theorem div_mod: \forall n,m:nat. 
-(lt O m) \to n=plus (times (div n m) m) (mod n m).
+theorem div_mod: \forall n,m:nat. O < m \to n=(div n m)*m+(mod n m).
 intros 2.elim m.elim (not_le_Sn_O O H).
 simplify.
 apply div_aux_mod_aux.
 qed.
 
 inductive div_mod_spec (n,m,q,r:nat) : Prop \def
-div_mod_spec_intro: 
-(lt r m) \to n=plus (times q m) r \to (div_mod_spec n m q r).
+div_mod_spec_intro: r < m \to n=q*m+r \to (div_mod_spec n m q r).
 
 (* 
 definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
-\lambda n,m,q,r:nat.(And (lt r m) n=plus (times q m) r).
+\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 Not (m=O).
+theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to \lnot m=O.
 intros 4.simplify.intros.elim H.absurd le (S r) O.
 rewrite < H1.assumption.
 exact not_le_Sn_O r.
 qed.
 
 theorem div_mod_spec_div_mod: 
-\forall n,m. (lt O m) \to (div_mod_spec n m (div n m) (mod n m)).
+\forall n,m. O < m \to (div_mod_spec n m (div n m) (mod n m)).
 intros.
 apply div_mod_spec_intro.
 apply lt_mod_m_m.assumption.
@@ -125,12 +123,12 @@ theorem div_mod_spec_to_eq :\forall a,b,q,r,q1,r1.
 intros.elim H.elim H1.
 apply nat_compare_elim q q1.intro.
 apply False_ind.
-cut eq nat (plus (times (minus q1 q) b) r1) r.
-cut le b (plus (times (minus q1 q) b) r1).
-cut le b r.
+cut eq nat ((q1-q)*b+r1) r.
+cut b \leq (q1-q)*b+r1.
+cut b \leq r.
 apply lt_to_not_le r b H2 Hcut2.
 elim Hcut.assumption.
-apply trans_le ? (times (minus q1 q) b) ?.
+apply trans_le ? ((q1-q)*b) ?.
 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.
@@ -153,12 +151,12 @@ intros.assumption.
 (* the following case is symmetric *)
 intro.
 apply False_ind.
-cut eq nat (plus (times (minus q q1) b) r) r1.
-cut le b (plus (times (minus q q1) b) r).
-cut le b r1.
+cut eq nat ((q-q1)*b+r) r1.
+cut b \leq (q-q1)*b+r.
+cut b \leq r1.
 apply lt_to_not_le r1 b H4 Hcut2.
 elim Hcut.assumption.
-apply trans_le ? (times (minus q q1) b) ?.
+apply trans_le ? ((q-q1)*b) ?.
 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index b4cff5d58..7ba20e821 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -26,29 +26,29 @@ let rec minus n m \def
 	[O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]].
 
+interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
 
-theorem minus_n_O: \forall n:nat.n=minus n O.
+theorem minus_n_O: \forall n:nat.n=n-O.
 intros.elim n.simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-theorem minus_n_n: \forall n:nat.O=minus n n.
+theorem minus_n_n: \forall n:nat.O=n-n.
 intros.elim n.simplify.
 reflexivity.
 simplify.apply H.
 qed.
 
-theorem minus_Sn_n: \forall n:nat. S O = minus (S n) n.
+theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
 intro.elim n.
 simplify.reflexivity.
 elim H.reflexivity.
 qed.
 
-theorem minus_Sn_m: \forall n,m:nat. 
-le m n \to minus (S n) m = S (minus n m).
+theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
 intros 2.
 apply nat_elim2
-(\lambda n,m.le m n \to minus (S n) m = S (minus n m)).
+(\lambda n,m.m \leq n \to (S n)-m = S (n-m)).
 intros.apply le_n_O_elim n1 H.
 simplify.reflexivity.
 intros.simplify.reflexivity.
@@ -57,10 +57,10 @@ apply le_S_S_to_le. assumption.
 qed.
 
 theorem plus_minus:
-\forall n,m,p:nat. le m n \to plus (minus n m) p = minus (plus n p) m.
+\forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
 intros 2.
 apply nat_elim2
-(\lambda n,m.\forall p:nat.le m n \to plus (minus n m) p = minus (plus n p) m).
+(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m).
 intros.apply le_n_O_elim ? H.
 simplify.rewrite < minus_n_O.reflexivity.
 intros.simplify.reflexivity.
@@ -68,9 +68,9 @@ intros.simplify.apply H.apply le_S_S_to_le.assumption.
 qed.
 
 theorem plus_minus_m_m: \forall n,m:nat.
-le m n \to n = plus (minus n m) m.
+m \leq n \to n = (n-m)+m.
 intros 2.
-apply nat_elim2 (\lambda n,m.le m n \to n = plus (minus n m) m).
+apply nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m).
 intros.apply le_n_O_elim n1 H.
 reflexivity.
 intros.simplify.rewrite < plus_n_O.reflexivity.
@@ -79,16 +79,16 @@ apply eq_f.rewrite < sym_plus.apply H.
 apply le_S_S_to_le.assumption.
 qed.
 
-theorem minus_to_plus :\forall n,m,p:nat.le m n \to minus n m = p \to 
-n = plus m p.
-intros.apply trans_eq ? ? (plus (minus n m) m) ?.
+theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
+n = m+p.
+intros.apply trans_eq ? ? ((n-m)+m) ?.
 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.
 qed.
 
-theorem plus_to_minus :\forall n,m,p:nat.le m n \to
-n = plus m p \to minus n m = p.
+theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
+n = m+p \to n-m = p.
 intros.
 apply inj_plus_r m.
 rewrite < H1.
@@ -98,9 +98,9 @@ apply plus_minus_m_m.assumption.
 qed.
 
 theorem eq_minus_n_m_O: \forall n,m:nat.
-le n m \to minus n m = O.
+n \leq m \to n-m = O.
 intros 2.
-apply nat_elim2 (\lambda n,m.le n m \to minus n m = O).
+apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
 (* ancora problemi con il not *)
@@ -109,7 +109,7 @@ intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.
 
-theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n).
+theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 intros.elim H.elim minus_Sn_n n.apply le_n.
 rewrite > minus_Sn_m.
 apply le_S.assumption.
@@ -117,9 +117,9 @@ apply lt_to_le.assumption.
 qed.
 
 (*
-theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)).
+theorem le_plus_minus: \forall n,m,p. n+m \leq p \to n \leq p-m.
 intros 3.
-elim p.simplify.apply trans_le ? (plus n m) ?.
+elim p.simplify.apply trans_le ? (n+m) ?.
 elim sym_plus ? ?.
 apply plus_le.assumption.
 apply le_n_Sm_elim ? ? H1.
@@ -130,11 +130,10 @@ theorem distributive_times_minus: distributive nat times minus.
 simplify.
 intros.
 apply (leb_elim z y).intro.
-cut plus (times x (minus y z)) (times x z) =
-    plus (minus (times x y) (times x z)) (times x z).
-apply inj_plus_l (times x z).
+cut x*(y-z)+x*z = (x*y-x*z)+x*z.
+apply inj_plus_l (x*z).
 assumption.
-apply trans_eq nat ? (times x y).
+apply trans_eq nat ? (x*y).
 rewrite < times_plus_distr. 
 rewrite < plus_minus_m_m ? ? H.reflexivity.
 rewrite < plus_minus_m_m ? ? ?.reflexivity.
@@ -142,7 +141,7 @@ apply le_times_r.
 assumption.
 intro.
 rewrite > eq_minus_n_m_O.
-rewrite > eq_minus_n_m_O (times x y).
+rewrite > eq_minus_n_m_O (x*y).
 rewrite < sym_times.simplify.reflexivity.
 apply lt_to_le.
 apply not_le_to_lt.assumption.
@@ -150,11 +149,10 @@ apply le_times_r.apply lt_to_le.
 apply not_le_to_lt.assumption.
 qed.
 
-theorem distr_times_minus: \forall n,m,p:nat.
-times n (minus m p) = minus (times n m) (times n p)
+theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 \def distributive_times_minus.
 
-theorem le_minus_m: \forall n,m:nat. le (minus n m) n.
+theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 intro.elim n.simplify.apply le_n.
 elim m.simplify.apply le_n.
 simplify.apply le_S.apply H.
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.
diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 3f788c650..5389418b5 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -22,14 +22,23 @@ inductive le (n:nat) : nat \to Prop \def
   | le_n : le n n
   | le_S : \forall m:nat. le n m \to le n (S m).
 
+interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
+alias symbol "leq" (instance 0) = "natural 'less or equal to'".
+
 definition lt: nat \to nat \to Prop \def
-\lambda n,m:nat.le (S n) m.
+\lambda n,m:nat.(S n) \leq m.
+
+interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
 
 definition ge: nat \to nat \to Prop \def
-\lambda n,m:nat.le m n.
+\lambda n,m:nat.m \leq n.
+
+interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
 
 definition gt: nat \to nat \to Prop \def
-\lambda n,m:nat.lt m n.
+\lambda n,m:nat.m<n.
+
+interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
 
 theorem transitive_le : transitive nat le.
 simplify.intros.elim H1.
@@ -37,89 +46,89 @@ assumption.
 apply le_S.assumption.
 qed.
 
-theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p
+theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 \def transitive_le.
 
-theorem le_S_S: \forall n,m:nat. le n m \to le (S n) (S m).
+theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m.
 intros.elim H.
 apply le_n.
 apply le_S.assumption.
 qed.
 
-theorem le_O_n : \forall n:nat. le O n.
+theorem le_O_n : \forall n:nat. O \leq n.
 intros.elim n.
 apply le_n.apply 
 le_S. assumption.
 qed.
 
-theorem le_n_Sn : \forall n:nat. le n (S n).
+theorem le_n_Sn : \forall n:nat. n \leq S n.
 intros. apply le_S.apply le_n.
 qed.
 
-theorem le_pred_n : \forall n:nat. le (pred n) n.
+theorem le_pred_n : \forall n:nat. pred n \leq n.
 intros.elim n.
 simplify.apply le_n.
 simplify.apply le_n_Sn.
 qed.
 
-theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m.
-intros.change with le (pred (S n)) (pred (S m)).
+theorem le_S_S_to_le : \forall n,m:nat. S n \leq S m \to n \leq m.
+intros.change with pred (S n) \leq pred (S m).
 elim H.apply le_n.apply trans_le ? (pred n1).assumption.
 apply le_pred_n.
 qed.
 
-theorem leS_to_not_zero : \forall n,m:nat. (le (S n) m ) \to not_zero m.
+theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
 intros.elim H.exact I.exact I.
 qed.
 
 (* not le *)
-theorem not_le_Sn_O: \forall n:nat. Not (le (S n) O).
+theorem not_le_Sn_O: \forall n:nat. \lnot (S n \leq O).
 intros.simplify.intros.apply leS_to_not_zero ? ? H.
 qed.
 
-theorem not_le_Sn_n: \forall n:nat. Not (le (S n) n).
-intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S n1) n1.
+theorem not_le_Sn_n: \forall n:nat. \lnot (S n \leq 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.
 qed.
 
 (* ??? this needs not le *)
-theorem S_pred: \forall n:nat.lt O n \to n=S (pred n).
+theorem S_pred: \forall n:nat.O<n \to n=S (pred n).
 intro.elim n.apply False_ind.exact not_le_Sn_O O H.
 apply eq_f.apply pred_Sn.
 qed.
 
 (* le vs. lt *)
-theorem lt_to_le : \forall n,m:nat. lt n m \to le n m.
+theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
 simplify.intros.elim H.
 apply le_S. apply le_n.
 apply le_S. assumption.
 qed.
 
-theorem not_le_to_lt: \forall n,m:nat. Not (le n m) \to lt m n.
+theorem not_le_to_lt: \forall n,m:nat. \lnot (n \leq m) \to m<n.
 intros 2.
-apply nat_elim2 (\lambda n,m.Not (le n m) \to lt m n).
-intros.apply absurd (le O n1).apply le_O_n.assumption.
+apply nat_elim2 (\lambda n,m.\lnot (n \leq 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. lt n m \to Not (le m n).
+theorem lt_to_not_le: \forall n,m:nat. n<m \to \lnot (m \leq n).
 simplify.intros 3.elim H.
 apply not_le_Sn_n n H1.
 apply H2.apply lt_to_le. apply H3.
 qed.
 
 (* le elimination *)
-theorem le_n_O_to_eq : \forall n:nat. (le n O) \to O=n.
+theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 intro.elim n.reflexivity.
 apply False_ind.
 (* non si applica not_le_Sn_O *)
 apply  (not_le_Sn_O ? H1).
 qed.
 
-theorem le_n_O_elim: \forall n:nat.le n O \to \forall P: nat \to Prop.
+theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
 P O \to P n.
 intro.elim n.
 assumption.
@@ -127,8 +136,8 @@ apply False_ind.
 apply  (not_le_Sn_O ? H1).
 qed.
 
-theorem le_n_Sm_elim : \forall n,m:nat.le n (S m) \to 
-\forall P:Prop. (le (S n) (S m) \to P) \to (n=(S m) \to P) \to P.
+theorem le_n_Sm_elim : \forall n,m:nat.n \leq S m \to 
+\forall P:Prop. (S n \leq S m \to P) \to (n=S m \to P) \to P.
 intros 4.elim H.
 apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
@@ -137,7 +146,7 @@ qed.
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.
 simplify.intros 2.
-apply nat_elim2 (\lambda n,m.((le n m) \to (le m n) \to n=m)).
+apply nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m)).
 intros.apply le_n_O_to_eq.assumption.
 intros.apply False_ind.apply not_le_Sn_O ? H.
 intros.apply eq_f.apply H.
@@ -145,12 +154,12 @@ apply le_S_S_to_le.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
-theorem antisym_le: \forall n,m:nat. le n m \to le m n \to n=m
+theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 \def antisymmetric_le.
 
-theorem decidable_le: \forall n,m:nat. decidable (le n m).
+theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
 intros.
-apply nat_elim2 (\lambda n,m.decidable (le n m)).
+apply nat_elim2 (\lambda n,m.decidable (n \leq m)).
 intros.simplify.left.apply le_O_n.
 intros.simplify.right.exact not_le_Sn_O n1.
 intros 2.simplify.intro.elim H.
diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma
index fbfad715c..bfb3668c7 100644
--- a/helm/matita/library/nat/orders_op.ma
+++ b/helm/matita/library/nat/orders_op.ma
@@ -20,40 +20,39 @@ include "nat/orders.ma".
 
 (* plus *)
 theorem monotonic_le_plus_r: 
-\forall n:nat.monotonic nat le (\lambda m.plus n m).
+\forall n:nat.monotonic nat le (\lambda m.n+m).
 simplify.intros.elim n.
 simplify.assumption.
 simplify.apply le_S_S.assumption.
 qed.
 
-theorem le_plus_r: \forall p,n,m:nat. le n m \to le (plus p n) (plus p m)
+theorem le_plus_r: \forall p,n,m:nat. n \leq m \to p+n \leq p+m
 \def monotonic_le_plus_r.
 
 theorem monotonic_le_plus_l: 
-\forall m:nat.monotonic nat le (\lambda n.plus n m).
+\forall m:nat.monotonic nat le (\lambda n.n+m).
 simplify.intros.
 rewrite < sym_plus.rewrite < sym_plus m.
 apply le_plus_r.assumption.
 qed.
 
-theorem le_plus_l: \forall p,n,m:nat. le n m \to le (plus n p) (plus m p)
+theorem le_plus_l: \forall p,n,m:nat. n \leq m \to n+p \leq m+p
 \def monotonic_le_plus_l.
 
-theorem le_plus: \forall n1,n2,m1,m2:nat. le n1 n2  \to le m1 m2 
-\to le (plus n1 m1) (plus n2 m2).
+theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \leq n2  \to m1 \leq m2 
+\to n1+m1 \leq n2+m2.
 intros.
-apply trans_le ? (plus n2 m1).
+apply trans_le ? (n2+m1).
 apply le_plus_l.assumption.
 apply le_plus_r.assumption.
 qed.
 
-theorem le_plus_n :\forall n,m:nat. le m (plus n m).
-intros.change with le (plus O m) (plus n m).
+theorem le_plus_n :\forall n,m:nat. m \leq n+m.
+intros.change with O+m \leq n+m.
 apply le_plus_l.apply le_O_n.
 qed.
 
-theorem eq_plus_to_le: \forall n,m,p:nat.n=plus m p
-\to le m n.
+theorem eq_plus_to_le: \forall n,m,p:nat.n=m+p \to m \leq n.
 intros.rewrite > H.
 rewrite < sym_plus.
 apply le_plus_n.
@@ -61,7 +60,7 @@ qed.
 
 (* times *)
 theorem monotonic_le_times_r: 
-\forall n:nat.monotonic nat le (\lambda m.times n m).
+\forall n:nat.monotonic nat le (\lambda m.n*m).
 simplify.intros.elim n.
 simplify.apply le_O_n.
 simplify.apply le_plus.
@@ -69,28 +68,28 @@ assumption.
 assumption.
 qed.
 
-theorem le_times_r: \forall p,n,m:nat. le n m \to le (times p n) (times p m)
+theorem le_times_r: \forall p,n,m:nat. n \leq m \to p*n \leq p*m
 \def monotonic_le_times_r.
 
 theorem monotonic_le_times_l: 
-\forall m:nat.monotonic nat le (\lambda n.times n m).
+\forall m:nat.monotonic nat le (\lambda n.n*m).
 simplify.intros.
 rewrite < sym_times.rewrite < sym_times m.
 apply le_times_r.assumption.
 qed.
 
-theorem le_times_l: \forall p,n,m:nat. le n m \to le (times n p) (times m p)
+theorem le_times_l: \forall p,n,m:nat. n \leq m \to n*p \leq m*p
 \def monotonic_le_times_l.
 
-theorem le_times: \forall n1,n2,m1,m2:nat. le n1 n2  \to le m1 m2 
-\to le (times n1 m1) (times n2 m2).
+theorem le_times: \forall n1,n2,m1,m2:nat. n1 \leq n2  \to m1 \leq m2 
+\to n1*m1 \leq n2*m2.
 intros.
-apply trans_le ? (times n2 m1).
+apply trans_le ? (n2*m1).
 apply le_times_l.assumption.
 apply le_times_r.assumption.
 qed.
 
-theorem le_times_n: \forall n,m:nat.le (S O) n \to le m (times n m).
+theorem le_times_n: \forall n,m:nat.S O \leq n \to m \leq n*m.
 intros.elim H.simplify.
 elim (plus_n_O ?).apply le_n.
 simplify.rewrite < sym_plus.apply le_plus_n.
diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 39e48f21e..6067ebcdc 100644
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -21,13 +21,16 @@ let rec plus n m \def
  [ O \Rightarrow m
  | (S p) \Rightarrow S (plus p m) ].
 
-theorem plus_n_O: \forall n:nat. n = plus n O.
+interpretation "natural plus" 'plus x y = (cic:/matita/nat/plus/plus.con x y).
+alias symbol "plus" (instance 0) = "natural plus".
+
+theorem plus_n_O: \forall n:nat. n = n+O.
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 
-theorem plus_n_Sm : \forall n,m:nat. S (plus n  m) = plus n (S m).
+theorem plus_n_Sm : \forall n,m:nat. S (n+m) = n+(S m).
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.assumption.
@@ -38,7 +41,7 @@ and functions/symmetric; functions symmetric is not in
 functions.moo why?
 theorem symmetric_plus: symmetric nat plus. *)
 
-theorem sym_plus: \forall n,m:nat. plus n m = plus m n.
+theorem sym_plus: \forall n,m:nat. n+m = m+n.
 intros.elim n.
 simplify.apply plus_n_O.
 simplify.rewrite > H.apply plus_n_Sm.
@@ -50,19 +53,19 @@ simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 
-theorem assoc_plus : \forall n,m,p:nat. plus (plus n m) p = plus n (plus m p)
+theorem assoc_plus : \forall n,m,p:nat. (n+m)+p = n+(m+p)
 \def associative_plus.
 
-theorem injective_plus_r: \forall n:nat.injective nat nat (\lambda m.plus n m).
+theorem injective_plus_r: \forall n:nat.injective nat nat (\lambda m.n+m).
 intro.simplify.intros 2.elim n.
 exact H.
 apply H.apply inj_S.apply H1.
 qed.
 
-theorem inj_plus_r: \forall p,n,m:nat. plus p n = plus p m \to n=m
+theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
 \def injective_plus_r.
 
-theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.plus n m).
+theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m).
 intro.simplify.intros.
 (* qui vorrei applicare injective_plus_r *)
 apply inj_plus_r m.
@@ -71,5 +74,5 @@ rewrite < sym_plus y.
 assumption.
 qed.
 
-theorem inj_plus_l: \forall p,n,m:nat. plus n p = plus m p \to n=m
+theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
 \def injective_plus_l.
diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 035116d0f..24a756dc5 100644
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -21,21 +21,23 @@ include "nat/plus.ma".
 let rec times n m \def 
  match n with 
  [ O \Rightarrow O
- | (S p) \Rightarrow (plus m (times p m)) ].
+ | (S p) \Rightarrow (m+(times p m)) ].
 
-theorem times_n_O: \forall n:nat. O = times n O.
+interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
+
+theorem times_n_O: \forall n:nat. O = n*O.
 intros.elim n.
 simplify.reflexivity.
 simplify.assumption.
 qed.
 
 theorem times_n_Sm : 
-\forall n,m:nat.plus n (times n  m) = times n (S m).
+\forall n,m:nat.n+n*m = n*(S m).
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.rewrite < H.
-transitivity (plus (plus n1 m) (times n1 m)).symmetry.apply assoc_plus.
-transitivity (plus (plus m n1) (times n1 m)).
+transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
+transitivity ((m+n1)+n1*m).
 apply eq_f2.
 apply sym_plus.
 reflexivity.
@@ -46,7 +48,7 @@ qed.
 theorem symmetric_times : symmetric nat times. *)
 
 theorem sym_times : 
-\forall n,m:nat.times n m = times m n.
+\forall n,m:nat.n*m = m*n.
 intros.elim n.
 simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.
@@ -61,7 +63,6 @@ apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
 rewrite > assoc_plus.reflexivity.
 qed.
 
-variant times_plus_distr: \forall n,m,p:nat.
-times n (plus m p) = plus (times n m) (times n p)
+variant times_plus_distr: \forall n,m,p:nat. n*(m+p)=n*m+n*p
 \def distributive_times_plus.
 
-- 
2.39.2