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