-distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
-change with \forall n,y,z.
-eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
+distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
+change with (\forall n,y,z.
+(pos n) * (y + z) = (pos n) * y + (pos n) * z).