def bit_mod

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:337

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/math/natural/arith.bend as NR

337def bit_mod(+n: Nat) -> {C.bit(n) == Nat.mod(n, 2n) : Nat}:
338  match n:
339    case 0n:
340      {==}
341    case 1n:
342      {==}
343    case 2n+ +q:
344      Equal.trans(Nat, C.bit(q), Nat.mod(q, 2n), Nat.mod(2n+q, 2n), bit_mod(q), Equal.sym(Nat, Nat.mod(2n+q, 2n), Nat.mod(q, 2n), NR.absorb(1n, 1n, q)))