proposition: Theorem FLX_format_FIX : forall x e, (bpow (e - 1) <= Rabs x <= bpow e)%R -> FIX_format beta (e - prec) x -> FLX_format x.
proof: Proof. Proof with auto with typeclass_instances. intros x e Hx Fx. apply FLX_format_generic. apply generic_format_FIX in Fx. revert Fx. apply generic_inclusion with (e := e)... apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE