law u32_cmp_to_nat

bend-mathlib@0.8.1.0 · u32.bend:529

import Base

529# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b).
530law u32_cmp_to_nat:
531  for a: U32
532  for b: U32
533  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}