proposition: Theorem id_p_ulp_le_bpow : forall x e, (0 < x)%R -> F x -> (x < bpow e)%R -> (x + ulp x <= bpow e)%R.
proof: Proof. intros x e Zx Fx Hx. 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_plus_distr_r. rewrite <- plus_IZR. apply F2R_p1_le_bpow. apply gt_0_F2R with beta (cexp beta fexp x). now rewrite <- Fx. now rewrite <- Fx. now apply Rgt_not_eq. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop