proposition: Lemma nearbyint_UP_correct : forall mode x, valid_ub (nearbyint_UP mode x) = true /\ le_upper (Xnearbyint mode (toX x)) (toX (nearbyint_UP mode x)).
proof: Proof. intros mode x. unfold nearbyint_UP. case_eq (real x); intro Hx; [ |now unfold nearbyint; rewrite Hx]. split. { rewrite valid_ub_correct. generalize (classify_correct (nearbyint infinity mode x)). rewrite real_correct. rewrite <-(nearbyint_correct _ _ _ Hx). unfold Xlift; simpl. revert Hx; rewrite real_correct. now case toX; [ |case classify]. } rewrite <-(nearbyint_correct _ _ _ Hx). now case toX; [ |intro x'; right]. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig