F64fmod.shq: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as F64fmod
Lines 62-70 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend&start_line=62&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/math/natural/misc.bend as MS
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

# N 2^t = (Q 2^t) B + r 2^t for N = Q B + r
def shq(+N0: Nat, +bp: Nat, +t: Nat) -> {C.shift(t, N0) == Nat.add(Nat.mul(C.shift(t, Nat.div(N0, 1n+bp)), 1n+bp), C.shift(t, Nat.mod(N0, 1n+bp))) : Nat}:
  +B = Nat.add(1n, bp)
  +Q = Nat.div(N0, B)
  +r = Nat.mod(N0, B)
  +e1 = Equal.cong(Nat, Nat, u => C.shift(t, u), N0, Nat.add(Nat.mul(Q, B), r), MS.divmod_eq(N0, bp))
  +e2 = WW.shift_add(t, Nat.mul(Q, B), r)
  +e3 = Equal.cong(Nat, Nat, u => Nat.add(u, C.shift(t, r)), C.shift(t, Nat.mul(Q, B)), Nat.mul(C.shift(t, Q), B), Equal.sym(Nat, Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mul(Q, B)), WW.shift_mul_l(t, Q, B)))
  Equal.trans(Nat, C.shift(t, N0), C.shift(t, Nat.add(Nat.mul(Q, B), r)), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, r)), e1, Equal.trans(Nat, C.shift(t, Nat.add(Nat.mul(Q, B), r)), Nat.add(C.shift(t, Nat.mul(Q, B)), C.shift(t, r)), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, r)), e2, e3))

Uses (12):
  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/math/natural/misc.bend&name=divmod_eq
  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_mul_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift