Notation for equality used everywhere.

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

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 953b3a1b630321187f46f9c2199e8b3dde12a928..035116d0f54d7312ce9fa676a9e31ea1af8226b6 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -23,14 +23,14 @@ let rec times n m \def
  [ O \Rightarrow O
  | (S p) \Rightarrow (plus m (times p m)) ].
 
-theorem times_n_O: \forall n:nat. eq nat O (times n O).
+theorem times_n_O: \forall n:nat. O = times n O.
 intros.elim n.
 simplify.reflexivity.
 simplify.assumption.
 qed.
 
 theorem times_n_Sm : 
-\forall n,m:nat. eq nat (plus n (times n  m)) (times n (S m)).
+\forall n,m:nat.plus n (times n  m) = times n (S m).
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.rewrite < H.
@@ -46,7 +46,7 @@ qed.
 theorem symmetric_times : symmetric nat times. *)
 
 theorem sym_times : 
-\forall n,m:nat. eq nat (times n m) (times m n).
+\forall n,m:nat.times n m = times m n.
 intros.elim n.
 simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.
@@ -62,6 +62,6 @@ rewrite > assoc_plus.reflexivity.
 qed.
 
 variant times_plus_distr: \forall n,m,p:nat.
-eq nat (times n (plus m p)) (plus (times n m) (times n p))
+times n (plus m p) = plus (times n m) (times n p)
 \def distributive_times_plus.