U32div.digit_one: 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 40-49 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=40&end_line=49

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/u32alg.bend as A
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 subtracting digit: (1 + 2q) b + d == a + 2 (q b + r) when b + d == a + 2 r
def digit_one(+q: Nat, +bn: Nat, +r: Nat, +a: Nat, +d: Nat, +h: {Nat.add(bn, d) == Nat.add(a, Nat.double(r)) : Nat}) -> {Nat.add(Nat.mul(1n+Nat.double(q), bn), d) == 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(bn, _), d) == rhs : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(bn, x), d), Nat.add(Nat.add(bn, d), x), A.add_rot(bn, x, d)) : {_ == rhs : Nat}
  %N.add_comm(x, Nat.add(bn, d)) : {_ == rhs : Nat}
  %Equal.sym(Nat, Nat.add(bn, d), Nat.add(a, Nat.double(r)), h) : {Nat.add(x, _) == 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 (11):
  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_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_double
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=add_rot