proposition: Theorem pred_UP_eq_DN : forall x, ~ F x -> (pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Fx. apply Rle_antisym. now apply pred_UP_le_DN. apply pred_ge_gt; try apply generic_format_round... pose proof round_DN_UP_lt _ _ _ Fx as HE. now apply Rlt_trans with (1 := proj1 HE) (2 := proj2 HE). Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop