(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/plus".
-
include "Z/z.ma".
include "nat/minus.ma".
rewrite < Zplus_z_OZ.
rewrite < (Zplus_z_OZ y).
rewrite < (Zplus_Zopp x).
-rewrite < (Zplus_Zopp x).
rewrite < assoc_Zplus.
rewrite < assoc_Zplus.
apply eq_f2