proposition: Theorem generic_format_FIX : forall x, FIX_format x -> generic_format beta FIX_exp x.
proof: Proof. intros x [[xm xe] Hx1 Hx2]. rewrite Hx1. now apply generic_format_canonical. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Ulp Round_NE