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_bzero_monus: (all x:UInt. bzero ∸ x = bzero)

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)))

uint_monus_bzero: (all n:UInt. n ∸ bzero = n)

auto uint_monus_cancel

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

uint_monus_cancel_bzero: (all n:UInt. n ∸ n = bzero)

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

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_pred_monus: (all n:UInt. pred(n) = n ∸ 1)