proposition: Lemma u_eq: F2R u= round beta fexp Zceil x.
proof: Proof. Proof with auto with typeclass_instances. apply Rnd_UP_pt_unique with (generic_format beta fexp) x... apply round_UP_pt... Qed.
imports: Coq(ZArith Reals Psatz) Core Operations