proposition: Theorem generic_format_FLT_FIX : forall x : R, (Rabs x <= bpow (emin + prec))%R -> generic_format beta (FIX_exp emin) x -> generic_format beta FLT_exp x.
proof: Proof. Proof with auto with typeclass_instances. apply generic_inclusion_le... intros e He. unfold FIX_exp. apply Z.max_lub. lia. apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE