F64divd.two: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divd.bend as F64divd
Lines 58-70 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divd.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divd.bend&start_line=58&end_line=70

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/proofs/lib/logic.bend as L
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/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

# two digits: r * 2^64 = (q1 * 2^32 + q2) * b + r2
def two(+bp: Nat, +R: Nat, +q1: Nat, +r1: Nat, +q2: Nat, +r2: Nat, +e1: {q1 == Nat.div(C.shift(32n, R), 1n+bp) : Nat}, +f1: {r1 == Nat.mod(C.shift(32n, R), 1n+bp) : Nat}, +e2: {q2 == Nat.div(C.shift(32n, r1), 1n+bp) : Nat}, +f2: {r2 == Nat.mod(C.shift(32n, r1), 1n+bp) : Nat}) -> {Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2) == C.shift(64n, R) : Nat}:
  +E1 = L.subst(Nat, w => {C.shift(32n, R) == Nat.add(Nat.mul(q1, 1n+bp), w) : Nat}, Nat.mod(C.shift(32n, R), 1n+bp), r1, Equal.sym(Nat, r1, Nat.mod(C.shift(32n, R), 1n+bp), f1), L.subst(Nat, w => {C.shift(32n, R) == Nat.add(Nat.mul(w, 1n+bp), Nat.mod(C.shift(32n, R), 1n+bp)) : Nat}, Nat.div(C.shift(32n, R), 1n+bp), q1, Equal.sym(Nat, q1, Nat.div(C.shift(32n, R), 1n+bp), e1), NR.dm_eq(bp, C.shift(32n, R))))
  +E2 = L.subst(Nat, w => {C.shift(32n, r1) == Nat.add(Nat.mul(q2, 1n+bp), w) : Nat}, Nat.mod(C.shift(32n, r1), 1n+bp), r2, Equal.sym(Nat, r2, Nat.mod(C.shift(32n, r1), 1n+bp), f2), L.subst(Nat, w => {C.shift(32n, r1) == Nat.add(Nat.mul(w, 1n+bp), Nat.mod(C.shift(32n, r1), 1n+bp)) : Nat}, Nat.div(C.shift(32n, r1), 1n+bp), q2, Equal.sym(Nat, q2, Nat.div(C.shift(32n, r1), 1n+bp), e2), NR.dm_eq(bp, C.shift(32n, r1))))
  +s1 = WW.shift_comp(32n, 32n, R)
  +s2 = Equal.cong(Nat, Nat, w => C.shift(32n, w), C.shift(32n, R), Nat.add(Nat.mul(q1, 1n+bp), r1), E1)
  +s3 = WW.shift_add(32n, Nat.mul(q1, 1n+bp), r1)
  +s4 = Equal.cong(Nat, Nat, w => Nat.add(w, C.shift(32n, r1)), C.shift(32n, Nat.mul(q1, 1n+bp)), Nat.mul(C.shift(32n, q1), 1n+bp), sh_mul(32n, q1, 1n+bp))
  +s5 = Equal.cong(Nat, Nat, w => Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), w), C.shift(32n, r1), Nat.add(Nat.mul(q2, 1n+bp), r2), E2)
  +s6 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), r2), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.add(Nat.mul(q2, 1n+bp), r2)), NA.add_assoc(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp), r2))
  +s7 = Equal.cong(Nat, Nat, w => Nat.add(w, r2), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), Equal.sym(Nat, Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), NA.mul_add_right(C.shift(32n, q1), q2, 1n+bp)))
  +ch = Equal.trans(Nat, C.shift(64n, R), C.shift(32n, C.shift(32n, R)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s1, Equal.trans(Nat, C.shift(32n, C.shift(32n, R)), C.shift(32n, Nat.add(Nat.mul(q1, 1n+bp), r1)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s2, Equal.trans(Nat, C.shift(32n, Nat.add(Nat.mul(q1, 1n+bp), r1)), Nat.add(C.shift(32n, Nat.mul(q1, 1n+bp)), C.shift(32n, r1)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s3, Equal.trans(Nat, Nat.add(C.shift(32n, Nat.mul(q1, 1n+bp)), C.shift(32n, r1)), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), C.shift(32n, r1)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s4, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), C.shift(32n, r1)), Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.add(Nat.mul(q2, 1n+bp), r2)), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s5, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.add(Nat.mul(q2, 1n+bp), r2)), Nat.add(Nat.add(Nat.mul(C.shift(32n, q1), 1n+bp), Nat.mul(q2, 1n+bp)), r2), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), s6, s7))))))
  Equal.sym(Nat, C.shift(64n, R), Nat.add(Nat.mul(Nat.add(C.shift(32n, q1), q2), 1n+bp), r2), ch)

Uses (16):
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  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/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divd.bend&name=sh_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift