Bits.and_step: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend as Bits
Lines 23-51 of bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend&start_line=23&end_line=51

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/random/rand.bend as SR
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/typed/width.bend as WI

# one bit and the rest: (b + 2a) & (c + 2d) = b c + 2 (a & d)
def and_step(+p: Nat, +b: Nat, +a: Nat, +c: Nat, +d: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +hc: {Nat.is_le(c, 1n) == True{} : Bool}) -> {SR.and_bits(1n+p, Nat.add(b, Nat.double(a)), Nat.add(c, Nat.double(d))) == Nat.add(Nat.mul(b, c), Nat.double(SR.and_bits(p, a, d))) : Nat}:
  match b c:
    case 0n 0n:
      %Equal.sym(Nat, C.bit(Nat.double(a)), 0n, WI.bit_dbl(0n, a)) : {Nat.add(Nat.mul(_, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, C.half(Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(Nat.double(a)), a, WI.half_dbl(0n, a)) : {Nat.add(Nat.mul(0n, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, _, C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(Nat.double(d)), d, WI.half_dbl(0n, d)) : {Nat.add(Nat.mul(0n, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      {==}
    case 0n 1n:
      %Equal.sym(Nat, C.bit(Nat.double(a)), 0n, WI.bit_dbl(0n, a)) : {Nat.add(Nat.mul(_, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, C.half(Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(Nat.double(a)), a, WI.half_dbl(0n, a)) : {Nat.add(Nat.mul(0n, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, _, C.half(1n+Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(1n+Nat.double(d)), d, WI.half_dbl(1n, d)) : {Nat.add(Nat.mul(0n, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      {==}
    case 1n 0n:
      %Equal.sym(Nat, C.bit(1n+Nat.double(a)), 1n, WI.bit_dbl(1n, a)) : {Nat.add(Nat.mul(_, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.bit(Nat.double(d)), 0n, WI.bit_dbl(0n, d)) : {Nat.add(Nat.mul(1n, _), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(1n+Nat.double(a)), a, WI.half_dbl(1n, a)) : {Nat.add(Nat.mul(1n, 0n), Nat.double(SR.and_bits(p, _, C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(Nat.double(d)), d, WI.half_dbl(0n, d)) : {Nat.add(Nat.mul(1n, 0n), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      {==}
    case 1n 1n:
      %Equal.sym(Nat, C.bit(1n+Nat.double(a)), 1n, WI.bit_dbl(1n, a)) : {Nat.add(Nat.mul(_, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.bit(1n+Nat.double(d)), 1n, WI.bit_dbl(1n, d)) : {Nat.add(Nat.mul(1n, _), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(1n+Nat.double(a)), a, WI.half_dbl(1n, a)) : {Nat.add(Nat.mul(1n, 1n), Nat.double(SR.and_bits(p, _, C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      %Equal.sym(Nat, C.half(1n+Nat.double(d)), d, WI.half_dbl(1n, d)) : {Nat.add(Nat.mul(1n, 1n), Nat.double(SR.and_bits(p, a, _))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
      {==}
    case 2n+q _:
      Empty.absurd({SR.and_bits(1n+p, Nat.add(2n+q, Nat.double(a)), Nat.add(c, Nat.double(d))) == Nat.add(Nat.mul(2n+q, c), Nat.double(SR.and_bits(p, a, d))) : Nat}, L.false_true(hb))
    case _ 2n+q:
      Empty.absurd({SR.and_bits(1n+p, Nat.add(b, Nat.double(a)), Nat.add(2n+q, Nat.double(d))) == Nat.add(Nat.mul(b, 2n+q), Nat.double(SR.and_bits(p, a, d))) : Nat}, L.false_true(hc))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=half_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend&name=and_bits