import UInt

import Base

import IntDefs

import IntAddSub

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

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

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

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

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

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

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