proposition: Theorem round_DN_ge_UP_gt : forall x y, F y -> (y < round beta fexp Zceil x -> y <= round beta fexp Zfloor x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fy Hlt. apply round_DN_pt... apply Rnot_lt_le. contradict Hlt. apply RIneq.Rle_not_lt. apply round_UP_pt... now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop