def bl_pos

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

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/lib/u32.bend as U
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

67def bl_pos(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}, +c: Nat, +hc: {M.bit_length(n) == c : Nat}) -> {Nat.is_le(1n, c) == True{} : Bool}:
68  match c:
69    case 0n:
70      +h0 = L.subst(Nat, z => {Nat.is_lt(n, C.pow2(z)) == True{} : Bool}, M.bit_length(n), 0n, hc, BT.bit_length_lt(n))
71      +e0 = U.lt_one_zero(n, h0)
72      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, LW.true_ne_false(Equal.trans(Bool, True{}, Nat.is_eq(n, 0n), False{}, Equal.sym(Bool, Nat.is_eq(n, 0n), True{}, L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, 0n, n, Equal.sym(Nat, n, 0n, e0), {==})), hz)))
73    case 1n+ +cp:
74      N.zero_le(cp)