Definition x : float 2 :=
   {| Fnum := 7205759403792794; Fexp := -56 |}.
Definition y : float 10 :=
   {| Fnum := 1; Fexp := -1 |}.
Definition F2R (f : float beta) :=
   (Fnum f) * beta ^ (Fexp f).