proposition: Lemma succ_le_plus_ulp : forall { Hm : Monotone_exp fexp } x, (succ x <= x + ulp x)%R.
proof: Proof. intros Mexp x. destruct (Rle_or_lt 0 x) as [Px|Nx]; [now right; apply succ_eq_pos|]. replace (_ + _)%R with (- (-x - ulp x))%R by ring. unfold succ; rewrite (Rle_bool_false _ _ Nx), <-ulp_opp. apply Ropp_le_contravar; unfold pred_pos. destruct (Req_dec (-x) (bpow (mag beta (-x) - 1))) as [Hx|Hx]. { rewrite (Req_bool_true _ _ Hx). apply (Rplus_le_reg_r x); ring_simplify; apply Ropp_le_contravar. unfold ulp; rewrite Req_bool_false; [|lra]. apply bpow_le, Mexp; lia. } now rewrite (Req_bool_false _ _ Hx); right. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop