law bit_zero_div

lawful-words@0.1.0.0 · proof_bytes.bend:73

import Base
import lawful-words@0.1.0.0/defs.bend as D

73# A word below 2^k has bit k clear.
74law bit_zero_div:
75  for +b: U32
76  for +k: Nat
77  for +h: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
78  {D.bit(b, k) == False{} : Bool}