proposition: Theorem ulp_FLT_gt : forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
proof: Proof. intros x; case (Req_dec x 0); intros Hx. rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0. rewrite Rabs_R0; apply bpow_gt_0. rewrite ulp_neq_0; try exact Hx. unfold cexp, FLT_exp. apply Rlt_le_trans with (bpow (mag beta x)*bpow (-prec))%R. apply Rmult_lt_compat_r. apply bpow_gt_0. now apply bpow_mag_gt. rewrite <- bpow_plus. apply bpow_le. apply Z.le_max_l. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE