law word_cmp_nat

bend-kit-lemmas@0.1.1.0 · lemmas.bend:84

import Base

84# Comparing two words compares their values.
85law word_cmp_nat:
86  for n: Nat
87  for a: Word(n)
88  for b: Word(n)
89  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}