W64div.dstep: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64div
Lines 162-164 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend&start_line=162&end_line=164

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

# one digit of long division: (A D + r) b + g == (A b + q2) D + r2 when r b + g == q2 D + r2
def dstep(+A: Nat, +D: Nat, +r: Nat, +b: Nat, +g: Nat, +q2: Nat, +r2: Nat, +e: {Nat.add(Nat.mul(r, b), g) == Nat.add(Nat.mul(q2, D), r2) : Nat}) -> {Nat.add(Nat.mul(Nat.add(Nat.mul(A, D), r), b), g) == Nat.add(Nat.mul(Nat.add(Nat.mul(A, b), q2), D), r2) : Nat}:
  Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Nat.mul(A, D), r), b), g), Nat.add(Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.mul(r, b)), g), Nat.add(Nat.mul(Nat.add(Nat.mul(A, b), q2), D), r2), Equal.cong(Nat, Nat, z => Nat.add(z, g), Nat.mul(Nat.add(Nat.mul(A, D), r), b), Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.mul(r, b)), NA.mul_add_right(Nat.mul(A, D), r, b)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.mul(r, b)), g), Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.add(Nat.mul(r, b), g)), Nat.add(Nat.mul(Nat.add(Nat.mul(A, b), q2), D), r2), NA.add_assoc(Nat.mul(Nat.mul(A, D), b), Nat.mul(r, b), g), Equal.trans(Nat, Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.add(Nat.mul(r, b), g)), Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.add(Nat.mul(q2, D), r2)), Nat.add(Nat.mul(Nat.add(Nat.mul(A, b), q2), D), r2), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.mul(A, D), b), z), Nat.add(Nat.mul(r, b), g), Nat.add(Nat.mul(q2, D), r2), e), Equal.trans(Nat, Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.add(Nat.mul(q2, D), r2)), Nat.add(Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.mul(q2, D)), r2), Nat.add(Nat.mul(Nat.add(Nat.mul(A, b), q2), D), r2), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.mul(q2, D)), r2), Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.add(Nat.mul(q2, D), r2)), NA.add_assoc(Nat.mul(Nat.mul(A, D), b), Nat.mul(q2, D), r2)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(Nat.mul(A, D), b), Nat.mul(q2, D)), r2), Nat.add(Nat.add(Nat.mul(Nat.mul(A, b), D), Nat.mul(q2, D)), r2), Nat.add(Nat.mul(Nat.add(Nat.mul(A, b), q2), D), r2), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, Nat.mul(q2, D)), r2), Nat.mul(Nat.mul(A, D), b), Nat.mul(Nat.mul(A, b), D), Equal.trans(Nat, Nat.mul(Nat.mul(A, D), b), Nat.mul(A, Nat.mul(D, b)), Nat.mul(Nat.mul(A, b), D), NA.mul_assoc(A, D, b), Equal.trans(Nat, Nat.mul(A, Nat.mul(D, b)), Nat.mul(A, Nat.mul(b, D)), Nat.mul(Nat.mul(A, b), D), Equal.cong(Nat, Nat, z => Nat.mul(A, z), Nat.mul(D, b), Nat.mul(b, D), NA.mul_comm(D, b)), Equal.sym(Nat, Nat.mul(Nat.mul(A, b), D), Nat.mul(A, Nat.mul(b, D)), NA.mul_assoc(A, b, D))))), Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.add(Nat.mul(Nat.mul(A, b), D), Nat.mul(q2, D)), Nat.mul(Nat.add(Nat.mul(A, b), q2), D), Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(A, b), q2), D), Nat.add(Nat.mul(Nat.mul(A, b), D), Nat.mul(q2, D)), NA.mul_add_right(Nat.mul(A, b), q2, D))))))))

Uses (10):
  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=Equal.trans
  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.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_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm