proposition: Theorem canonical_generic_format : forall x, generic_format x -> exists f : float beta, x = F2R f /\ canonical f.
proof: Proof. intros x Hx. rewrite Hx. eexists. apply (conj eq_refl). unfold canonical. now rewrite <- Hx. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop