law word_cmp_to_nat

bend-mathlib@0.8.1.0 · u32.bend:128

import Base

128# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b).
129law word_cmp_to_nat:
130  for n: Nat
131  for a: Word(n)
132  for b: Word(n)
133  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}