Integer_Mul: trait
  includes
    Integer_Add, Integer_Basics
  asserts with x, y, z: Int

    x * 0 = 0;
    x * 1 = x;
    x * 2 = x + x;
    x * succ(y) = (x*y) + x;
    x * pred(y) = (x*y) + (-x);

    (y + z) * x = (x * y) + (x * z);
    (-y) * x = -(x * y);