F64cmp.xsh: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as F64cmp
Lines 107-119 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&start_line=107&end_line=119

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/math/typed/width.bend as WW

# 2^xexp = 2^1925 * 2^e' with e' = max(E, 1)
def xsh(+E: Nat, +b: Bool, +m: Nat) -> {C.shift(SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), m) == C.shift(1925n, C.shift(SF.pick(Nat, b, 1n, E), m)) : Nat}:
  match b:
    case True{}:
      # each step is stated in the goal's own terms: a conversion that
      # unfolded C.shift(1925n, _) would walk 1925 doublings per level
      +e1 = Equal.cong(Nat, Nat, z => C.shift(z, m), SF.pick(Nat, True{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), Nat.add(1925n, 1n), {==})
      +e2 = Equal.cong(Nat, Nat, z => C.shift(1925n, C.shift(z, m)), 1n, SF.pick(Nat, True{}, 1n, E), {==})
      Equal.trans(Nat, C.shift(SF.pick(Nat, True{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), m), C.shift(Nat.add(1925n, 1n), m), C.shift(1925n, C.shift(SF.pick(Nat, True{}, 1n, E), m)), e1, Equal.trans(Nat, C.shift(Nat.add(1925n, 1n), m), C.shift(1925n, C.shift(1n, m)), C.shift(1925n, C.shift(SF.pick(Nat, True{}, 1n, E), m)), WW.shift_comp(1925n, 1n, m), e2))
    case False{}:
      +e1 = Equal.cong(Nat, Nat, z => C.shift(z, m), SF.pick(Nat, False{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), Nat.add(1925n, E), esub(E))
      +e2 = Equal.cong(Nat, Nat, z => C.shift(1925n, C.shift(z, m)), E, SF.pick(Nat, False{}, 1n, E), {==})
      Equal.trans(Nat, C.shift(SF.pick(Nat, False{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), m), C.shift(Nat.add(1925n, E), m), C.shift(1925n, C.shift(SF.pick(Nat, False{}, 1n, E), m)), e1, Equal.trans(Nat, C.shift(Nat.add(1925n, E), m), C.shift(1925n, C.shift(E, m)), C.shift(1925n, C.shift(SF.pick(Nat, False{}, 1n, E), m)), WW.shift_comp(1925n, E, m), e2))

Uses (11):
  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.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&name=esub
  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=zb