law word_cmp_to_nat_sym

bend-mathlib@0.8.1.0 · u32.bend:985

import Base

985# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
986law word_cmp_to_nat_sym:
987  for n: Nat
988  for a: Word(n)
989  for b: Word(n)
990  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}