~/jendhub

def ucmp_lt

bend-kit-collections@0.1.4.1 · PROOF.bend:4006

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
import Base

4006def ucmp_lt(+x: U32, +y: U32, e: {U32.cmp(x, y) == LT{} : Cmp}) -> {Nat.cmp(U32.to_nat(x), U32.to_nat(y)) == LT{} : Cmp}:
4007  Equal.trans(Cmp, Nat.cmp(U32.to_nat(x), U32.to_nat(y)), U32.cmp(x, y), LT{}, ucmp_nat(x, y), e)

Uses (7)

Used by (1)