Arith.step: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as Arith
Lines 96-106 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&start_line=96&end_line=106

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

# one long-division step: if x == q d + r and 2^k r + y == q2 d + r2 then
# 2^k x + y == (2^k q + q2) d + r2
def step(+k: Nat, +q: Nat, +r: Nat, +d: Nat, +y: Nat, +q2: Nat, +r2: Nat, +x: Nat, +hx: {x == Nat.add(Nat.mul(q, d), r) : Nat}, +h2: {Nat.add(sc(k, r), y) == Nat.add(Nat.mul(q2, d), r2) : Nat}) -> {Nat.add(sc(k, x), y) == Nat.add(Nat.mul(Nat.add(sc(k, q), q2), d), r2) : Nat}:
  +rhs = Nat.add(Nat.mul(Nat.add(sc(k, q), q2), d), r2)
  %Equal.sym(Nat, x, Nat.add(Nat.mul(q, d), r), hx) : {Nat.add(sc(k, _), y) == rhs : Nat}
  %A.sc_add(k, Nat.mul(q, d), r) : {Nat.add(_, y) == rhs : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(sc(k, Nat.mul(q, d)), sc(k, r)), y), Nat.add(sc(k, Nat.mul(q, d)), Nat.add(sc(k, r), y)), N.add_assoc(sc(k, Nat.mul(q, d)), sc(k, r), y)) : {_ == rhs : Nat}
  %Equal.sym(Nat, Nat.add(sc(k, r), y), Nat.add(Nat.mul(q2, d), r2), h2) : {Nat.add(sc(k, Nat.mul(q, d)), _) == rhs : Nat}
  %Equal.sym(Nat, sc(k, Nat.mul(q, d)), Nat.mul(sc(k, q), d), sc_mul(k, q, d)) : {Nat.add(_, Nat.add(Nat.mul(q2, d), r2)) == rhs : Nat}
  %Equal.sym(Nat, Nat.mul(Nat.add(sc(k, q), q2), d), Nat.add(Nat.mul(sc(k, q), d), Nat.mul(q2, d)), NA.mul_add_right(sc(k, q), q2, d)) : {Nat.add(Nat.mul(sc(k, q), d), Nat.add(Nat.mul(q2, d), r2)) == Nat.add(_, r2) : Nat}
  Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(sc(k, q), d), Nat.mul(q2, d)), r2), Nat.add(Nat.mul(sc(k, q), d), Nat.add(Nat.mul(q2, d), r2)), N.add_assoc(Nat.mul(sc(k, q), d), Nat.mul(q2, d), r2))

Uses (9):
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=sc_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@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-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=sc_add