add_assoc: (all m:Nat, n:Nat, o:Nat. (m + n) + o = m + (n + o))

add_both_sides_of_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y = x + z) ⇔ (y = z))))

add_commute: (all n:Nat. (all m:Nat. n + m = m + n))

auto add_zero

assoc_add: (all m:Nat, n:Nat, o:Nat. m + (n + o) = (m + n) + o)

left_cancel: (all x:Nat. (all y:Nat, z:Nat. (if x + y = x + z then y = z)))

auto lit_idem

lit_idem: (all x:Nat. lit(lit(x)) = lit(x))

auto lit_suc_add

lit_suc_add: (all x:Nat, y:Nat. lit(suc(x)) + lit(y) = lit(suc(lit(x) + lit(y))))

auto nat_add_zero

nat_add_zero: (all x:Nat. x + ℕ0 = x)

nat_suc_one_add: (all n:Nat. suc(n) = ℕ1 + n)

auto nat_zero_add

nat_zero_add: (all y:Nat. ℕ0 + y = y)

auto suc_lit

suc_lit: (all n:Nat. suc(lit(n)) = lit(suc(n)))

auto zero_add