proposition: Theorem ulp_FLT_0 : ulp beta FLT_exp 0 = bpow emin.
proof: Proof. unfold ulp. rewrite Req_bool_true by easy. case negligible_exp_spec. - intros T. elim Zle_not_lt with (2 := T emin). apply Z.le_max_r. - intros n Hn. apply f_equal. assert (H: FLT_exp emin = emin). apply Z.max_r. generalize (prec_gt_0 prec). clear ; lia. rewrite <- H. apply fexp_negligible_exp_eq. apply FLT_exp_valid. exact Hn. rewrite H. apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE