def bl_le_c

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

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/proofs/lib/nat.bend as N

551# n < 2^K gives bit_length(n) <= K
552def bl_le_c(+K: Nat, +bl: Nat, +h: {Nat.is_lt(C.pow2(bl), C.pow2(1n+K)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(1n+K, bl) == c : Bool}) -> {Nat.is_le(bl, K) == True{} : Bool}:
553  match c:
554    case True{}:
555      Empty.absurd({Nat.is_le(bl, K) == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(C.pow2(bl), C.pow2(1n+K)), False{}, Equal.sym(Bool, Nat.is_lt(C.pow2(bl), C.pow2(1n+K)), True{}, h), N.le_not_lt(C.pow2(bl), C.pow2(1n+K), N.pow2_mono(1n+K, bl, hc)))))
556    case False{}:
557      N.lt_succ_le(bl, K, N.not_le_lt(1n+K, bl, hc))