proposition: Theorem generic_format_FLT_FLX : forall x : R, (bpow (emin + prec - 1) <= Rabs x)%R -> generic_format beta (FLX_exp prec) x -> generic_format beta FLT_exp x.
proof: Proof. intros x Hx H. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0. apply generic_format_0. unfold generic_format, scaled_mantissa. now rewrite cexp_FLT_FLX. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE