proposition: Theorem round_UP_pt : forall x, Rnd_UP_pt generic_format x (round Zceil x).
proof: Proof. intros x. rewrite <- (Ropp_involutive x). rewrite round_UP_opp. apply Rnd_UP_pt_opp. apply generic_format_opp. apply round_DN_pt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop