law word

stelliferous@0.0.2.0 · proofs/u32_comparison.bend:51

import Base

51law word:
52  for +n: Nat
53  for +a: Word(n)
54  for +b: Word(n)
55  {Word.cmp(n,a,b) == Nat.cmp(Word.to_nat(n,a),Word.to_nat(n,b)) : Cmp}