fromNat_mult: (all x:Nat, y:Nat. fromNat(x * y) = fromNat(x) * fromNat(y))

auto lit_mult_fromNat

lit_mult_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) * fromNat(lit(y)) = fromNat(lit(x) * lit(y)))

toNat_mult: (all x:UInt, y:UInt. toNat(x * y) = toNat(x) * toNat(y))

uint_dist_mult_add: (all a:UInt, x:UInt, y:UInt. a * (x + y) = a * x + a * y)

uint_dist_mult_add_right: (all x:UInt, y:UInt, a:UInt. (x + y) * a = x * a + y * a)

uint_mult_assoc: (all m:UInt, n:UInt, o:UInt. (m * n) * o = m * (n * o))

uint_mult_commute: (all m:UInt, n:UInt. m * n = n * m)

uint_mult_mono_le: (all n:UInt, x:UInt, y:UInt. (if x ≤ y then n * x ≤ n * y))

uint_mult_mono_le2: (all n:UInt, x:UInt, m:UInt, y:UInt. (if (n ≤ m and x ≤ y) then n * x ≤ m * y))

auto uint_mult_one

uint_mult_one: (all n:UInt. n * 1 = n)

uint_mult_to_zero: (all n:UInt, m:UInt. (if n * m = 0 then (n = 0 or m = 0)))

auto uint_mult_zero

uint_mult_zero: (all n:UInt. n * 0 = 0)

auto uint_one_mult

uint_one_mult: (all n:UInt. 1 * n = n)

uint_pos_mult_both_sides_of_less: (all n:UInt, x:UInt, y:UInt. (if (0 < n and x < y) then n * x < n * y))

uint_two_mult: (all n:UInt. 2 * n = n + n)

auto uint_zero_mult

uint_zero_mult: (all n:UInt. 0 * n = 0)