def is_le_nat

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sqrt.bend:66

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U

66def is_le_nat(+a: U32, +b: U32) -> {U32.is_le(a, b) == Nat.is_le(v(a), v(b)) : Bool}:
67  %Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(v(a), v(b)), U.u32_cmp(a, b)) : {Cmp.is_le(_) == Nat.is_le(v(a), v(b)) : Bool}
68  {==}