def glb

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:54

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

54# a normal G is at least 2^E * 2^52
55def 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}:
56  +ec = Equal.trans(Nat, c, 1n, one, hc, Equal.sym(Nat, one, 1n, h1))
57  +e1 = Equal.cong(Nat, Nat, z => C.shift(52n, z), c, one, ec)
58  +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))
59  +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)
60  WW.shift_mono(E, C.shift(52n, one), Nat.add(F, C.shift(52n, c)), h2)