F64cmp.glb: 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 54-60 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=54&end_line=60

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/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

# a normal G is at least 2^E * 2^52
def glb(+one: Nat, +h1: {one == 1n : Nat}, +E: Nat, +c: Nat, +hc: {c == 1n : Nat}, +F: Nat) -> {Nat.is_le(C.shift(E, C.shift(52n, one)), C.shift(E, Nat.add(F, C.shift(52n, c)))) == True{} : Bool}:
  +ec = Equal.trans(Nat, c, 1n, one, hc, Equal.sym(Nat, one, 1n, h1))
  +e1 = Equal.cong(Nat, Nat, z => C.shift(52n, z), c, one, ec)
  +h0 = L.subst(Nat, z => {Nat.is_le(C.shift(52n, one), z) == True{} : Bool}, Nat.add(C.shift(52n, one), F), Nat.add(F, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), F), N.le_add_right(C.shift(52n, one), F))
  +h2 = L.subst(Nat, z => {Nat.is_le(C.shift(52n, one), Nat.add(F, z)) == True{} : Bool}, C.shift(52n, one), C.shift(52n, c), Equal.sym(Nat, C.shift(52n, c), C.shift(52n, one), e1), h0)
  WW.shift_mono(E, C.shift(52n, one), Nat.add(F, C.shift(52n, c)), h2)

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