proposition: Lemma nearbyint_correct : forall mode x, toX (nearbyint mode x) = Xnearbyint mode (toX x).
proof: Proof. intros mode x. unfold toX. destruct x as [|mx ex] ; try easy. simpl. generalize (mantissa_sign_correct mx). case (mantissa_sign mx). - rewrite toF_zero. simpl. now rewrite (Rnearbyint_IZR mode 0). intros s m [_ H]. rewrite <- Fnearbyint_exact_correct. rewrite round_at_exp_aux_correct; try easy. unfold Fnearbyint_exact. eapply f_equal. eapply f_equal2; try easy. now rewrite exponent_zero_correct. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig