auto lit_monus_fromNat

lit_monus_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) ∸ fromNat(lit(y)) = fromNat(lit(x) ∸ lit(y)))

toNat_monus: (all x:UInt, y:UInt. toNat(x ∸ y) = toNat(x) ∸ toNat(y))

uint_add_both_monus: (all z:UInt, y:UInt, x:UInt. (z + y) ∸ (z + x) = y ∸ x)

auto uint_add_monus_identity

uint_add_monus_identity: (all m:UInt, n:UInt. (m + n) ∸ m = n)

uint_dist_mult_monus: (all x:UInt. (all y:UInt, z:UInt. x * (y ∸ z) = x * y ∸ x * z))

uint_le_exists_monus: (all n:UInt, m:UInt. (if n ≤ m then some x:UInt. m = n + x))

uint_monus_add_assoc: (all n:UInt, l:UInt, m:UInt. (if m ≤ n then l + (n ∸ m) = (l + n) ∸ m))

uint_monus_add_identity: (all n:UInt. (all m:UInt. (if m ≤ n then m + (n ∸ m) = n)))

auto uint_monus_cancel

uint_monus_cancel: (all n:UInt. n ∸ n = 0)

uint_monus_monus_eq_monus_add: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = x ∸ (y + z))

uint_monus_one_less: (all n:UInt. (if not (n = 0) then n ∸ 1 < n))

uint_monus_order: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = (x ∸ z) ∸ y)

auto uint_monus_zero

uint_monus_zero: (all n:UInt. n ∸ 0 = n)

uint_monus_zero_iff_less_eq: (all x:UInt, y:UInt. ((x ≤ y) ⇔ (x ∸ y = 0)))