proposition: Theorem ulp_FLT_le : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> (ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R.
proof: Proof. intros x Hx. assert (Zx : (x <> 0)%R). intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt. rewrite Z, Rabs_R0; apply bpow_gt_0. rewrite ulp_neq_0 with (1 := Zx). unfold cexp, FLT_exp. destruct (mag beta x) as (e,He). apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R. rewrite <- bpow_plus. right; apply f_equal. replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring. apply Z.max_l; simpl. cut (emin+prec-1 < e)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=Hx). now apply He. apply Rmult_le_compat_r. apply bpow_ge_0. now apply He. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE