proposition: Lemma round_N_plus_ulp_ge : forall { Hm : Monotone_exp fexp } choice1 choice2 x, let rx := round beta fexp (Znearest choice2) x in (x <= round beta fexp (Znearest choice1) (rx + ulp rx))%R.
proof: Proof. intros Hm choice1 choice2 x. simpl. set (rx := round _ _ _ x). assert (Vrnd1 : Valid_rnd (Znearest choice1)) by now apply valid_rnd_N. assert (Vrnd2 : Valid_rnd (Znearest choice2)) by now apply valid_rnd_N. apply (Rle_trans _ (succ rx)); [now apply succ_round_ge_id|]. rewrite round_generic; [now apply succ_le_plus_ulp|now simpl|]. now apply generic_format_plus_ulp, generic_format_round. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop