proposition: Lemma negligible_exp_FLT : exists n, negligible_exp FLT_exp = Some n /\ (n <= emin)%Z.
proof: Proof. case (negligible_exp_spec FLT_exp). { intro H; exfalso; specialize (H emin); revert H. apply Zle_not_lt, Z.le_max_r. } intros n Hn; exists n; split; [now simpl|]. destruct (Z.max_spec (n - prec) emin) as [(Hm, Hm')|(Hm, Hm')]. { now revert Hn; unfold FLT_exp; rewrite Hm'. } revert Hn prec_gt_0_; unfold FLT_exp, Prec_gt_0; rewrite Hm'; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE