law hk_step

lawful-fields@0.1.1.0 · proof_digits.bend:529

import Base

529# n <= BK(1 + j) gives n / 10 <= BK(j).
530law hk_step:
531  for +n: U32
532  for +j: Nat
533  for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(1n+j))) == True{} : Bool}
534  {Nat.is_le(U32.to_nat(U32.div(n, 10)), U32.to_nat(BK(j))) == True{} : Bool}