law hkb

lawful-fields@0.1.1.0 · proof_digits.bend:703

import Base

703law hkb:
704  for +n: U32
705  for +r: Nat
706  {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(9n+r))) == True{} : Bool}