def s_ge

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mexp.bend:60

import Base
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/math/typed/f64round.bend as FR

60def s_ge(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.is_le(8088n, Nat.add(ea, eb)) == True{} : Bool}:
61  +ha = eg(ea, sa, Xx, n2x, hsa, hXx)
62  +hb = eg(eb, sb, Xy, n2y, hsb, hXy)
63  N.le_trans(8088n, Nat.add(4044n, eb), Nat.add(ea, eb), N.le_add_left(4044n, eb, 4044n, hb), Equal.trans(Bool, Nat.is_le(Nat.add(4044n, eb), Nat.add(ea, eb)), Nat.is_le(4044n, ea), True{}, FR.le_cancel_r(4044n, ea, eb), ha))