proposition: Lemma nearbyint_correct : forall mode, extension (Rnearbyint mode) (I.nearbyint mode).
proof: Proof. intros mode xi x. now apply I.nearbyint_correct. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic