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;
zero_times:    integer(X) => X * 0 = 0;
division:      integer(X) and
               integer(Y) and
               integer(Z) and
               X * Y = X * Z and
               not (X = 0) =>
               Y = Z;
prove:         integer(X) and