proposition: Theorem round_DN_eq : forall x d, F d -> (d <= x < succ d)%R -> round beta fexp Zfloor x = d.
proof: Proof. Proof with auto with typeclass_instances. intros x d Fd (Hxd1,Hxd2). generalize (round_DN_pt beta fexp x); intros (T1,(T2,T3)). apply sym_eq, Rle_antisym. now apply T3. destruct (generic_format_EM beta fexp x) as [Fx|NFx]. rewrite round_generic... apply succ_le_inv; try assumption. apply succ_le_lt; try assumption. apply generic_format_succ... apply succ_le_inv; try assumption. rewrite succ_DN_eq_UP; trivial. apply round_UP_pt... apply generic_format_succ... now left. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop