def nbit_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:338

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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

338def nbit_c(+c: Nat, +h2: {Nat.is_eq(C.half(c), 0n) == True{} : Bool}) -> {Nat.sub(1n, c) == SF.b2n(Bool.not(Bool.not(Nat.is_eq(c, 0n)))) : Nat}:
339  match c:
340    case 0n:
341      {==}
342    case 1n:
343      {==}
344    case 2n+ +q:
345      Empty.absurd({Nat.sub(1n, 2n+q) == SF.b2n(Bool.not(Bool.not(Nat.is_eq(2n+q, 0n)))) : Nat}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h2)))