def u.le_of_lt
import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrderimport Base
323def u.le_of_lt(+a: U32, +b: U32, +e: {ult(a, b) == True{} : Bool}) -> {ule(a, b) == True{} : Bool}:
324 cm.le_of_lt(U32.cmp(a, b), e)
import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrderimport Base
323def u.le_of_lt(+a: U32, +b: U32, +e: {ult(a, b) == True{} : Bool}) -> {ule(a, b) == True{} : Bool}:
324 cm.le_of_lt(U32.cmp(a, b), e)