proposition: Lemma nearbyint_IZR : forall md x, @nearbyint md x = IZR ((round_mode md) x).
proof: Proof. unfold nearbyint, round, F2R, scaled_mantissa. simpl. intros md x. now rewrite 2Rmult_1_r. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)