def yn_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:344

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
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/math/typed/f64light.bend as FL

344# a scale above another double's is a normal number's
345def yn_c(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(SF.efield(y), 0n) == c : Bool}) -> {c == False{} : Bool}:
346  match c:
347    case True{}:
348      +h1 = L.subst(Bool, b => {Nat.is_lt(SF.xexp(x), SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(SF.efield(y), SF.zb()), 1075n))) == True{} : Bool}, Nat.is_eq(SF.efield(y), 0n), True{}, hc, hlt)
349      +h2 = N.le_not_lt(SF.xexp(x), 1926n, xge(x))
350      Empty.absurd({True{} == False{} : Bool}, FL.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(SF.xexp(x), 1926n), False{}, Equal.sym(Bool, Nat.is_lt(SF.xexp(x), 1926n), True{}, h1), h2)))
351    case False{}:
352      {==}