dist_mult_add: (all a:Nat, x:Nat, y:Nat. a * (x + y) = a * x + a * y)

dist_mult_add_right: (all x:Nat, y:Nat, a:Nat. (x + y) * a = x * a + y * a)

auto lit_mult_lit_suc

lit_mult_lit_suc: (all m:Nat, n:Nat. lit(m) * lit(suc(n)) = lit(m) + lit(m) * lit(n))

auto lit_mult_suc

lit_mult_suc: (all m:Nat, n:Nat. lit(m) * suc(n) = lit(m) + lit(m) * n)

auto lit_suc_mult

lit_suc_mult: (all m:Nat, n:Nat. lit(suc(m)) * lit(n) = lit(n) + lit(m) * lit(n))

lit_two_mult: (all n:Nat. ℕ2 * n = n + n)

mult_assoc: (all m:Nat. (all n:Nat, o:Nat. (m * n) * o = m * (n * o)))

mult_commute: (all m:Nat. (all n:Nat. m * n = n * m))

auto mult_one

auto mult_zero

auto nat_mult_one

nat_mult_one: (all n:Nat. n * ℕ1 = n)

auto nat_one_mult

nat_one_mult: (all n:Nat. ℕ1 * n = n)

auto nat_zero_mult

nat_zero_mult: (all y:Nat. ℕ0 * lit(y) = ℕ0)

auto one_mult

auto zero_mult