theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
intros.
theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
intros.