proposition: Theorem UP_le_succ_DN : forall x, (round beta fexp Zceil x <= succ (round beta fexp Zfloor x))%R.
proof: Proof. intros x. rewrite <- (Ropp_involutive x). rewrite round_DN_opp, round_UP_opp, succ_opp. apply Ropp_le_contravar. apply pred_UP_le_DN. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop