proposition: Lemma nearbyint_correct : forall mode, extension (Xnearbyint mode) (nearbyint mode).
proof: Proof. intros mode [|xl xu] [|xr] ; try ( intros ; exact I ) ; [now unfold convert; case (_ && _)|]. simpl. intros Hlu. generalize Hlu. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vu Vl [Hl Hu]. unfold convert. rewrite (proj1 (F.nearbyint_DN_correct _ _)). rewrite (proj1 (F.nearbyint_UP_correct _ _)). split. { xreal_tac2. generalize (F.nearbyint_DN_correct mode xl). rewrite X. unfold le_lower, le_upper; simpl. xreal_tac2; [easy|]; simpl. intros [_ H]. now apply (Rle_trans _ _ _ (Ropp_le_cancel _ _ H)), Rnearbyint_le. } xreal_tac2. generalize (F.nearbyint_UP_correct mode xu). rewrite X. unfold le_upper; simpl. xreal_tac2; [easy|]; simpl. intros [_ H]. now revert H; apply Rle_trans, Rnearbyint_le. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval