proposition: Theorem generic_N_pt_DN_or_UP : forall x f, Rnd_N_pt generic_format x f -> f = round Zfloor x \/ f = round Zceil x.
proof: Proof. intros x f Hxf. destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf). left. apply Rnd_DN_pt_unique with (1 := H). apply round_DN_pt. right. apply Rnd_UP_pt_unique with (1 := H). apply round_UP_pt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop