proposition: Theorem ulp_le_id: forall x, (0 < x)%R -> F x -> (ulp x <= x)%R.
proof: Proof. intros x Zx Fx. rewrite <- (Rmult_1_l (ulp x)). pattern x at 2; rewrite Fx. rewrite ulp_neq_0. 2: now apply Rgt_not_eq. unfold F2R; simpl. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le, (Zlt_le_succ 0). apply gt_0_F2R with beta (cexp beta fexp x). now rewrite <- Fx. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop