proposition: Theorem succ_DN_eq_UP : forall x, ~ F x -> (succ (round beta fexp Zfloor x) = round beta fexp Zceil x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Fx. rewrite <- pred_UP_eq_DN; trivial. rewrite succ_pred; trivial. apply generic_format_round... Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop