proposition: Theorem id_m_ulp_ge_bpow : forall x e, F x -> x <> ulp x -> (bpow e < x)%R -> (bpow e <= x - ulp x)%R.
proof: Proof. intros x e Fx Hx' Hx. assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z. assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. apply gt_0_F2R with beta (cexp beta fexp x). rewrite <- Fx. apply Rle_lt_trans with (2:=Hx). apply bpow_ge_0. lia. case (Zle_lt_or_eq _ _ H); intros Hm. pattern x at 1 ; rewrite Fx. rewrite ulp_neq_0. unfold F2R. simpl. pattern (bpow (cexp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. rewrite <- Rmult_minus_distr_r. rewrite <- minus_IZR. apply bpow_le_F2R_m1. easy. now rewrite <- Fx. apply Rgt_not_eq, Rlt_gt. apply Rlt_trans with (2:=Hx), bpow_gt_0. contradict Hx'. pattern x at 1; rewrite Fx. rewrite <- Hm. rewrite ulp_neq_0. unfold F2R; simpl. now rewrite Rmult_1_l. apply Rgt_not_eq, Rlt_gt. apply Rlt_trans with (2:=Hx), bpow_gt_0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop