proposition: Lemma Rnearbyint_le : forall mode x y, (x <= y)%R -> (Rnearbyint mode x <= Rnearbyint mode y)%R.
proof: Proof. intros mode x y Hxy. destruct mode ; simpl. now apply IZR_le, Zceil_le. now apply IZR_le, Zfloor_le. now apply IZR_le, Ztrunc_le. now apply IZR_le; destruct (valid_rnd_N (fun x => negb (Z.even x))); auto. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal