def bl_le

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:144

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as WC

144def bl_le(+k: Nat, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {Nat.is_le(M.bit_length(n), k) == True{} : Bool}:
145  match k:
146    case 0n:
147      +en = N.eq_from_is_eq(n, 0n, h)
148      %Equal.sym(Nat, n, 0n, en) : {Nat.is_le(M.bit_length(_), 0n) == True{} : Bool}
149      {==}
150    case 1n+ +kp:
151      match n:
152        case 0n:
153          {==}
154        case 1n+ +np:
155          %Equal.sym(Nat, M.bit_length(1n+np), 1n+M.bit_length(C.half(1n+np)), WC.bl_succ(np)) : {Nat.is_le(_, 1n+kp) == True{} : Bool}
156          bl_le(kp, C.half(1n+np), h)