proposition: Theorem ulp_FLX_le : forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.
proof: Proof. intros x; case (Req_dec x 0); intros Hx. rewrite Hx, ulp_FLX_0, Rabs_R0. right; ring. rewrite ulp_neq_0; try exact Hx. unfold cexp, FLX_exp. replace (mag beta x - prec)%Z with ((mag beta x - 1) + (1-prec))%Z by ring. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. now apply bpow_mag_le. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE