F64cmp.gub: 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 36-52 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=36&end_line=52

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

# G < 2^(1+E) * 2^52
def gub(+one: Nat, +h1: {one == 1n : Nat}, +E: Nat, +b: Bool, +hb: {Nat.is_eq(E, 0n) == b : Bool}, +c: Nat, +hc: {c == SF.b2n(Bool.not(b)) : Nat}, +F: Nat, +hF: {C.fits(52n, F) == True{} : Bool}) -> {Nat.is_lt(C.shift(SF.pick(Nat, b, 1n, E), Nat.add(F, C.shift(52n, c))), C.shift(1n+E, C.shift(52n, one))) == True{} : Bool}:
  match b:
    case True{}:
      +eE = N.eq_from_is_eq(E, 0n, hb)
      +ef = Equal.trans(Nat, Nat.add(F, C.shift(52n, c)), Nat.add(F, 0n), F, Equal.cong(Nat, Nat, z => Nat.add(F, C.shift(52n, z)), c, 0n, hc), N.add_zero(F))
      +h0 = WW.shift_lt(1n, F, C.shift(52n, one), WW.lt_one(52n, one, h1, F, hF))
      +h2 = L.subst(Nat, z => {Nat.is_lt(C.shift(1n, z), C.shift(1n, C.shift(52n, one))) == True{} : Bool}, F, Nat.add(F, C.shift(52n, c)), Equal.sym(Nat, Nat.add(F, C.shift(52n, c)), F, ef), h0)
      L.subst(Nat, z => {Nat.is_lt(C.shift(1n, Nat.add(F, C.shift(52n, c))), C.shift(1n+z, C.shift(52n, one))) == True{} : Bool}, 0n, E, Equal.sym(Nat, E, 0n, eE), h2)
    case False{}:
      +ec = Equal.trans(Nat, c, 1n, one, hc, Equal.sym(Nat, one, 1n, h1))
      +es = Equal.cong(Nat, Nat, z => Nat.add(F, C.shift(52n, z)), c, one, ec)
      +h0 = N.lt_add_r2(F, C.shift(52n, one), C.shift(52n, one), WW.lt_one(52n, one, h1, F, hF))
      +h1b = L.subst(Nat, z => {Nat.is_lt(Nat.add(F, C.shift(52n, one)), z) == True{} : Bool}, Nat.add(C.shift(52n, one), C.shift(52n, one)), Nat.double(C.shift(52n, one)), Equal.sym(Nat, Nat.double(C.shift(52n, one)), Nat.add(C.shift(52n, one), C.shift(52n, one)), NA.double_self(C.shift(52n, one))), h0)
      +h2 = WW.shift_lt(E, Nat.add(F, C.shift(52n, one)), Nat.double(C.shift(52n, one)), h1b)
      +h3 = L.subst(Nat, z => {Nat.is_lt(C.shift(E, Nat.add(F, C.shift(52n, one))), z) == True{} : Bool}, C.shift(E, Nat.double(C.shift(52n, one))), Nat.double(C.shift(E, C.shift(52n, one))), WW.shift_dbl(E, C.shift(52n, one)), h2)
      L.subst(Nat, z => {Nat.is_lt(C.shift(E, z), Nat.double(C.shift(E, C.shift(52n, one)))) == True{} : Bool}, Nat.add(F, C.shift(52n, one)), Nat.add(F, C.shift(52n, c)), Equal.sym(Nat, Nat.add(F, C.shift(52n, c)), Nat.add(F, C.shift(52n, one)), es), h3)

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self
  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=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=eq_from_is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_add_r2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  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=b2n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick