def bit_length_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/bits.bend:116

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

116def bit_length_zero() -> {M.bit_length(0n) == 0n : Nat}:
117  {==}