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. split; [easy|]. rewrite nearbyint_correct. unfold le_upper, toX. now case (Xlift _ _); [|intro r; right]. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig