def dexp_ge

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64tools.bend:189

import Base
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

189def dexp_ge(+x: F.F64) -> {Nat.is_le(63n, F.dexp(x)) == True{} : Bool}:
190  dge_z(F.exp_field(x), Nat.is_eq(F.exp_field(x), 0n))