law w_lt

lawful-arrays@0.1.0.0 · proof_words.bend:18

import Base

18law w_lt:
19  for +a: U32
20  for +b: U32
21  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}