| GT \Rightarrow (neg (pred (m-n)))]
| (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer plus" 'plus x y = (cic:/matita/library_autobatch/Z/plus/Zplus.con x y).
+interpretation "integer plus" 'plus x y = (Zplus x y).
theorem Zplus_z_OZ: \forall z:Z. z+OZ = z.
intro.
| (pos n) \Rightarrow (neg n)
| (neg n) \Rightarrow (pos n) ].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer unary minus" 'uminus x = (cic:/matita/library_autobatch/Z/plus/Zopp.con x).
+interpretation "integer unary minus" 'uminus x = (Zopp x).
theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
intros.
(* minus *)
definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
-interpretation "integer minus" 'minus x y = (cic:/matita/library_autobatch/Z/plus/Zminus.con x y).
+interpretation "integer minus" 'minus x y = (Zminus x y).