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