fact: Definition negligible_exp: option Z := match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with | inleft N => Some (proj1_sig N) | inright _ => None end.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop