U32div.digit_zero: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as U32div
Lines 51-57 of bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&start_line=51&end_line=57

import Base
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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as PR

# a zero digit: 2q b + (a + 2 r) == a + 2 (q b + r)
def digit_zero(+q: Nat, +bn: Nat, +r: Nat, +a: Nat) -> {Nat.add(Nat.mul(Nat.double(q), bn), Nat.add(a, Nat.double(r))) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}:
  +x = Nat.double(Nat.mul(q, bn))
  +rhs = Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r)))
  %Equal.sym(Nat, Nat.mul(Nat.double(q), bn), x, PR.double_product(q, bn)) : {Nat.add(_, Nat.add(a, Nat.double(r))) == rhs : Nat}
  %NA.add_swap(a, x, Nat.double(r)) : {_ == rhs : Nat}
  Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(x, Nat.double(r)), Nat.double(Nat.add(Nat.mul(q, bn), r)), N.add_double(Nat.mul(q, bn), r))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend&name=double_product
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_double