law bn_lt2

lawful-words@0.1.0.0 · proof_word.bend:25

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

25law bn_lt2:
26  for +b: Bool
27  {Nat.is_lt(N.bn(b), 2n) == True{} : Bool}