import Base

import Nat

import UIntDefs

import UIntToFrom

toNat_less: (all x:UInt, y:UInt. (if x < y then toNat(x) < toNat(y)))

toNat_less_equal: (all x:UInt, y:UInt. (if x ≤ y then toNat(x) ≤ toNat(y)))

less_toNat: (all x:UInt, y:UInt. (if toNat(x) < toNat(y) then x < y))

uint_less_equal_refl: (all n:UInt. n ≤ n)

uint_less_implies_less_equal: (all x:UInt, y:UInt. (if x < y then x ≤ y))

less_equal_toNat: (all x:UInt, y:UInt. (if toNat(x) ≤ toNat(y) then x ≤ y))

uint_less_irreflexive: (all x:UInt. not (x < x))

uint_less_trans: (all x:UInt, y:UInt, z:UInt. (if (x < y and y < z) then x < z))

uint_not_less_zero: (all x:UInt. not (x < 0))

uint_not_less_implies_less_equal: (all x:UInt, y:UInt. (if not (x < y) then y ≤ x))

uint_le_refl: (all x:UInt. x ≤ x)

uint_le_trans: (all x:UInt, y:UInt, z:UInt. (if (x ≤ y and y ≤ z) then x ≤ z))

uint_zero_le: (all x:UInt. 0 ≤ x)

uint_le_zero: (all x:UInt. (if x ≤ 0 then x = 0))