def lower

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

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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as BT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

79def lower(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(C.pow2(Nat.sub(M.bit_length(n), 1n)), n) == True{} : Bool}:
80  match n:
81    case 0n:
82      Empty.absurd({Nat.is_le(C.pow2(Nat.sub(M.bit_length(0n), 1n)), 0n) == True{} : Bool}, LW.true_ne_false(hz))
83    case 1n+ +np:
84      +B = M.bit_length(1n+np)
85      +eb = N.sub_add(B, 1n, bl_pos(1n+np, hz, B, {==}))
86      +h1 = L.subst(Nat, z => {Nat.is_le(C.pow2(z), Nat.double(1n+np)) == True{} : Bool}, B, 1n+Nat.sub(B, 1n), Equal.sym(Nat, 1n+Nat.sub(B, 1n), B, eb), BT.bit_length_le(np))
87      dle(C.pow2(Nat.sub(B, 1n)), 1n+np, h1)