law less_one_is_zero

stelliferous@0.0.2.0 · proofs/word_encoding.bend:137

import Base

137law less_one_is_zero:
138  for +n: Nat
139  for +w: Word(1n+n)
140  {Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})) == Cmp.is_eq(Word.cmp(1n+n,w,Word.zero(1n+n))) : Bool}