dist_neg_mult: (all x:Int, y:Int. - (x * y) = - x * y)

int_mult_assoc: (all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z))

int_mult_commute: (all x:Int, y:Int. x * y = y * x)

auto int_mult_one

int_mult_one: (all x:Int. x * +1 = x)

auto int_mult_zero

int_mult_zero: (all x:Int. x * +0 = +0)

auto int_one_mult

int_one_mult: (all x:Int. +1 * x = x)

auto int_zero_mult

int_zero_mult: (all x:Int. +0 * x = +0)