W64dm.ovq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend as W64dm
Lines 94-98 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&start_line=94&end_line=98

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU

# q b > x
def ovq(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +b: WU.U64, +q: U32) -> {X.over96(xl, xh, X.mul_32_64(q, b)) == Nat.is_lt(X96(xl, xh), Nat.mul(v(q), SW.value(b))) : Bool}:
  match b:
    case WU.U64{+bl, +bh}:
      Equal.trans(Bool, X.over96(xl, xh, (X.fst_q(X.mul_32_64(q, WU.U64{bl, bh})), X.snd_r(X.mul_32_64(q, WU.U64{bl, bh})))), Nat.is_lt(X96(xl, xh), Nat.add(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{bl, bh}))), C.shift(64n, v(X.snd_r(X.mul_32_64(q, WU.U64{bl, bh})))))), Nat.is_lt(X96(xl, xh), Nat.mul(v(q), SW.value(WU.U64{bl, bh}))), ov96(xl, xh, X.fst_q(X.mul_32_64(q, WU.U64{bl, bh})), X.snd_r(X.mul_32_64(q, WU.U64{bl, bh}))), Equal.cong(Nat, Bool, z => Nat.is_lt(X96(xl, xh), z), Nat.add(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{bl, bh}))), C.shift(64n, v(X.snd_r(X.mul_32_64(q, WU.U64{bl, bh}))))), Nat.mul(v(q), SW.value(WU.U64{bl, bh})), mul3264(one, h1, q, bl, bh)))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&name=X96
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&name=mul3264
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&name=ov96
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=fst_q
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=mul_32_64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=over96
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=snd_r