proposition: Theorem round_ZR_or_AW : forall x, round rnd x = round Ztrunc x \/ round rnd x = round Zaway x.
proof: Proof. intros x. unfold round. destruct (Zrnd_ZR_or_AW 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