proposition: Lemma round_N_eq_UP_pt: forall choice x d u, Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> ((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 Hd Hu H. assert (H0:(u = round beta fexp Zceil x)%R). apply Rnd_UP_pt_unique with (1:=Hu). apply round_UP_pt... rewrite H0. apply round_N_eq_UP. rewrite <- H0. rewrite Rnd_DN_pt_unique with F x (round beta fexp Zfloor x) d; try assumption. apply round_DN_pt... Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop