def u32.cmp_nat

bend-osdev-algo@0.1.0.0 · PROOF.bend:927

import Base

927def u32.cmp_nat(a: U32, b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
928  match a b:
929    case U32{wa} U32{wb}:
930      word.cmp_nat(32n, wa, wb)