law wlt.m

lawful-words@0.1.0.0 · proof_u32.bend:19

import Base

19law wlt.m:
20  for +w: Word(32n)
21  for +m: Nat
22  for +hm: {Nat.pow(2n, 32n) == m : Nat}
23  {Nat.is_lt(Word.to_nat(32n, w), m) == True{} : Bool}