proposition: Theorem FIX_format_generic : forall x, generic_format beta FIX_exp x -> FIX_format x.
proof: Proof. intros x H. rewrite H. eexists ; repeat split. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Ulp Round_NE