proposition: Lemma d_eq: F2R d= round beta fexp Zfloor x.
proof: Proof. Proof with auto with typeclass_instances. apply Rnd_DN_pt_unique with (generic_format beta fexp) x... apply round_DN_pt... Qed.
imports: Coq(ZArith Reals Psatz) Core Operations