def nz_bl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:188

import Base
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/natcmp.bend as NC

188def nz_bl(+m: Nat, +K: Nat, +hb: {Nat.is_le(1n+K, M.bit_length(m)) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {z == False{} : Bool}:
189  match z:
190    case True{}:
191      +e0 = N.eq_from_is_eq(m, 0n, hz)
192      +h0 = L.subst(Nat, w => {Nat.is_le(1n+K, M.bit_length(w)) == True{} : Bool}, m, 0n, e0, hb)
193      +h1 = L.subst(Nat, w => {Nat.is_le(1n+K, w) == True{} : Bool}, M.bit_length(0n), 0n, BT.bit_length_zero(), h0)
194      NC.absurd_tf({True{} == False{} : Bool}, h1)
195    case False{}:
196      {==}