def bl_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:175

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

175def bl_zero(+f: Nat, +k: Nat) -> {M.bit_length_go(f, 0n, k) == k : Nat}:
176  match f:
177    case 0n:
178      {==}
179    case 1n+g:
180      {==}