**** Experimental: ****

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

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index bb5ed67c5bdeb31bc2a98b000e1e92477eba3c9c..1352988df32cd32d2dcf77699db265a8c4f4c523 100644 (file)
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -31,14 +31,17 @@ definition Ztimes :Z \to Z \to Z \def
          | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
          | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
          
-theorem Ztimes_z_OZ:  \forall z:Z. eq Z (Ztimes z OZ) OZ.
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
+
+theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
 intro.elim z.
 simplify.reflexivity.
 simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-
+(*CSC: da qui in avanti niente notazione *)
 (*
 theorem symmetric_Ztimes : symmetric Z Ztimes.
 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
@@ -251,21 +254,4 @@ qed.
 
 variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
 \def associative_Zplus.
-
-definition Zopp : Z \to Z \def
-\lambda x:Z. match x with
-[ OZ \Rightarrow OZ
-| (pos n) \Rightarrow (neg n)
-| (neg n) \Rightarrow (pos n) ].
-
-theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
-intro.elim x.
-apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-qed.
 *)