proposition: Lemma u'_eq: (0 < F2R d)%R -> exists f:float beta, F2R f = F2R u /\ (Fexp f = Fexp d)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros Y. rewrite u_eq; unfold round. eexists; repeat split. simpl; now rewrite Fexp_d. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations