def xlt

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

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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

480def xlt(+x: F.F64, +y: F.F64, +b: Bool, +h: {Nat.is_lt(F.dexp(x), F.dexp(y)) == b : Bool}) -> {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == b : Bool}:
481  +h1 = L.subst(Nat, t => {Nat.is_lt(t, F.dexp(y)) == b : Bool}, F.dexp(x), SF.xexp(x), T.dexp_value(x), h)
482  L.subst(Nat, t => {Nat.is_lt(SF.xexp(x), t) == b : Bool}, F.dexp(y), SF.xexp(y), T.dexp_value(y), h1)