F64divq.lowq: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend as F64divq
Lines 30-34 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend&start_line=30&end_line=34

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

# the low two bits of Q come from its low digit
def lowq(+d1: U32, +d2: U32) -> {C.low(2n, v(d2)) == C.low(2n, SW.value(WU.U64{d2, d1})) : Nat}:
  +e1 = Equal.cong(Nat, Nat, z => Nat.add(v(d2), z), C.shift(32n, v(d1)), C.shift(2n, C.shift(30n, v(d1))), WW.shift_comp(2n, 30n, v(d1)))
  +e2 = WW.low_add_shift(2n, v(d2), C.shift(30n, v(d1)))
  Equal.sym(Nat, C.low(2n, SW.value(WU.U64{d2, d1})), C.low(2n, v(d2)), Equal.trans(Nat, C.low(2n, SW.value(WU.U64{d2, d1})), C.low(2n, Nat.add(v(d2), C.shift(2n, C.shift(30n, v(d1))))), C.low(2n, v(d2)), Equal.cong(Nat, Nat, z => C.low(2n, z), SW.value(WU.U64{d2, d1}), Nat.add(v(d2), C.shift(2n, C.shift(30n, v(d1)))), e1), e2))

Uses (13):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_add_shift
  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=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64