proposition: Theorem ulp_FLT_small : forall x, (Rabs x < bpow (emin + prec))%R -> ulp beta FLT_exp x = bpow emin.
proof: Proof. intros x Hx. destruct (Req_dec x 0%R) as [Zx|Zx]. { rewrite Zx. apply ulp_FLT_0. } rewrite ulp_neq_0 by easy. apply f_equal. apply Z.max_r. destruct (mag beta x) as [e He]. simpl. cut (e - 1 < emin + prec)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (2 := Hx). now apply He. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE