+theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
+intro.unfold Zone.simplify.
+elim z;simplify
+ [reflexivity
+ |rewrite < plus_n_O.reflexivity
+ |rewrite < plus_n_O.reflexivity
+ ]
+qed.
+
+theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
+intro.
+rewrite < sym_Ztimes.
+apply Ztimes_Zone_l.
+qed.
+