associativity: integer(X) and integer(Y) and integer(Z) =>
               X * (Y * Z) = (X * Y) * Z;
commutativity: integer(X) and integer(Y) => X * Y = Y * X;
factor:        integer(X) and integer(Y) and factor(X, Y) <=>
               exists(Z) and integer(Z) and X * Z = Y;
    
prove:         factor(X, Y) and factor(Y, Z) =>