def bl_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bl.bend:57

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

57def bl_le(+K: Nat, +n: Nat, +hn: {C.fits(K, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(M.bit_length(n), K) == c : Bool}) -> {c == True{} : Bool}:
58  match c:
59    case True{}:
60      {==}
61    case False{}:
62      +hk = N.lt_succ_le_succ(K, M.bit_length(n), N.not_le_lt(M.bit_length(n), K, hc))
63      +hp = N.pow2_mono(1n+K, M.bit_length(n), hk)
64      bl_le_n(K, n, hn, hp)