theorem symmetric_Ztimes : symmetric Z Ztimes.
change with (\forall x,y:Z. x*y = y*x).
intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
theorem symmetric_Ztimes : symmetric Z Ztimes.
change with (\forall x,y:Z. x*y = y*x).
intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.