Fround.qeq_f: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
Lines 332-347 of bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&start_line=332&end_line=347

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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

def qeq_f(+k: Nat, +m: Nat, +x: Nat, +u: Nat, +c1: Bool, +hc1: {Nat.is_le(x, u) == c1 : Bool}, +hc2: {Nat.is_le(Nat.add(x, k), u) == False{} : Bool}) -> {SF.pick(Nat, c1, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))) == C.shift(Nat.sub(Nat.add(x, k), u), m) : Nat}:
  match c1:
    case True{}:
      +t = Nat.sub(u, x)
      +eu = N.sub_add(u, x, hc1)
      +hlt0 = N.not_le_lt(Nat.add(x, k), u, hc2)
      +hlt1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, k)) == True{} : Bool}, u, Nat.add(x, t), Equal.sym(Nat, Nat.add(x, t), u, eu), hlt0)
      +hlt2 = Equal.trans(Bool, Nat.is_lt(t, k), Nat.is_lt(Nat.add(x, t), Nat.add(x, k)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(x, t), Nat.add(x, k)), Nat.is_lt(t, k), WW.lt_cancel_l(x, t, k)), hlt1)
      +htk = N.lt_le(t, k, hlt2)
      +es = NC.sh_split(k, t, m, htk)
      +e1 = Equal.trans(Nat, SF.rne(C.shift(k, m), t), SF.rne(C.shift(t, C.shift(Nat.sub(k, t), m)), t), C.shift(Nat.sub(k, t), m), Equal.cong(Nat, Nat, z => SF.rne(z, t), C.shift(k, m), C.shift(t, C.shift(Nat.sub(k, t), m)), es), rne_exact(t, C.shift(Nat.sub(k, t), m)))
      +e2 = Equal.trans(Nat, Nat.sub(k, t), Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(Nat.add(x, k), u), Equal.sym(Nat, Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(k, t), sub_cancel_r(k, t, x)), Equal.trans(Nat, Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(Nat.add(x, k), Nat.add(t, x)), Nat.sub(Nat.add(x, k), u), Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(t, x)), Nat.add(k, x), Nat.add(x, k), NA.add_comm(k, x)), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(x, k), z), Nat.add(t, x), u, Equal.trans(Nat, Nat.add(t, x), Nat.add(x, t), u, NA.add_comm(t, x), eu))))
      Equal.trans(Nat, SF.rne(C.shift(k, m), t), C.shift(Nat.sub(k, t), m), C.shift(Nat.sub(Nat.add(x, k), u), m), e1, Equal.cong(Nat, Nat, z => C.shift(z, m), Nat.sub(k, t), Nat.sub(Nat.add(x, k), u), e2))
    case False{}:
      +hux = N.lt_le(u, x, N.not_le_lt(x, u, hc1))
      Equal.trans(Nat, C.shift(Nat.sub(x, u), C.shift(k, m)), C.shift(Nat.add(Nat.sub(x, u), k), m), C.shift(Nat.sub(Nat.add(x, k), u), m), Equal.sym(Nat, C.shift(Nat.add(Nat.sub(x, u), k), m), C.shift(Nat.sub(x, u), C.shift(k, m)), WW.shift_comp(Nat.sub(x, u), k, m)), Equal.cong(Nat, Nat, z => C.shift(z, m), Nat.add(Nat.sub(x, u), k), Nat.sub(Nat.add(x, k), u), Equal.sym(Nat, Nat.sub(Nat.add(x, k), u), Nat.add(Nat.sub(x, u), k), sub_add_r(x, k, u, hux))))

Uses (23):
  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.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.is_le
  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.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  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/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=not_le_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=rne_exact
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=sub_add_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=sub_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=sh_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_cancel_l
  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
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=rne