proposition: Theorem round_UP_eq : forall x u, F u -> (pred u < x <= u)%R -> round beta fexp Zceil x = u.
proof: Proof. Proof with auto with typeclass_instances. intros x u Fu Hux. rewrite <- (Ropp_involutive (round beta fexp Zceil x)). rewrite <- round_DN_opp. rewrite <- (Ropp_involutive u). apply f_equal. apply round_DN_eq; try assumption. now apply generic_format_opp. split;[now apply Ropp_le_contravar|idtac]. rewrite succ_opp. now apply Ropp_lt_contravar. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop