Prove:

integer(X) and

Given:

integer(X) and integer(Y) and integer(Z) =>
X * (Y * Z) = (X * Y) * Z

and:

integer(X) and integer(Y) => X * Y = Y * X

and:

integer(X) => X * 0 = 0

and:

integer(X) and
integer(Y) and
integer(Z) and
X * Y = X * Z and
not (X = 0) =>
Y = Z

Test as a text file.