proposition: Lemma round_N_eq_UP: forall choice x, let d:=round beta fexp Zfloor x in let u:=round beta fexp Zceil x in ((d+u)/2 < x)%R -> round beta fexp (Znearest choice) x = u.
proof: Proof. Proof with auto with typeclass_instances. intros choice x d u H. apply Rle_antisym. apply round_le_generic; try apply round_UP_pt... destruct (generic_format_EM beta fexp x) as [Fx|Fx]. rewrite round_generic... apply round_UP_pt; trivial; now right. apply round_N_ge_midp. apply round_UP_pt... apply Rle_lt_trans with (2:=H). right; apply f_equal2; trivial; rewrite Rplus_comm; apply f_equal2; trivial. now apply pred_UP_eq_DN. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop