proposition: Theorem round_DN_or_UP : forall x, round rnd x = round Zfloor x \/ round rnd x = round Zceil x.
proof: Proof. intros x. unfold round. destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx]. left. now rewrite Hx. right. now rewrite Hx. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop