proposition: Theorem Zrnd_ZR_or_AW : forall x, rnd x = Ztrunc x \/ rnd x = Zaway x.
proof: Proof. intros x. unfold Ztrunc, Zaway. destruct (Zrnd_DN_or_UP x) as [Hx|Hx] ; case Rlt_bool. now right. now left. now left. now right. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop