proposition: Theorem round_ZR_pt : forall x, Rnd_ZR_pt generic_format x (round Ztrunc x).
proof: Proof. intros x. split ; intros Hx. rewrite round_ZR_DN with (1 := Hx). apply round_DN_pt. rewrite round_ZR_UP with (1 := Hx). apply round_UP_pt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop