proposition: Lemma succ_round_ge_id : forall rnd { Zrnd : Valid_rnd rnd } x, (x <= succ (round beta fexp rnd x))%R.
proof: Proof. intros rnd Vrnd x. apply (Rle_trans _ (round beta fexp Raux.Zceil x)). { now apply round_UP_pt. } destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr. { now apply UP_le_succ_DN. } apply succ_ge_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop