proposition: Lemma negligible_exp_FLX : negligible_exp FLX_exp = None.
proof: Proof. case (negligible_exp_spec FLX_exp). intros _; reflexivity. intros n H2; contradict H2. unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE