import Base

import Nat

import UIntDefs

import UIntToFrom

import UIntLess

import UIntAdd

import UIntMult

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

uint_zero_monus: (all x:UInt. 0 ∸ x = 0)

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

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

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

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)

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