law below_one_zero

stelliferous@0.0.2.0 · proofs/word_encoding.bend:254

import Base

254law below_one_zero:
255  for +n: Nat
256  for +w: Word(1n+n)
257  for below: {Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})) == True{} : Bool}
258  {w == Word.zero(1n+n) : Word(1n+n)}