def xexp_ge

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF

52def xexp_ge(+E: Nat) -> {Nat.is_le(1926n, SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))) == True{} : Bool}:
53  xg_c(E, Nat.is_eq(E, 0n), {==})