def bit_nz

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64m128.bend:41

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

41# a value below 2 is the bit "is nonzero"
42def bit_nz(+h: Nat, +hf: {C.fits(1n, h) == True{} : Bool}) -> {S.bit_value(Bool.not(Nat.is_eq(h, 0n))) == h : Nat}:
43  match h:
44    case 0n:
45      {==}
46    case 1n:
47      {==}
48    case 2n+z:
49      Empty.absurd({S.bit_value(Bool.not(Nat.is_eq(2n+z, 0n))) == 2n+z : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))