proposition: Theorem FLX_format_generic : forall x, generic_format beta FLX_exp x -> FLX_format x.
proof: Proof. intros x H. rewrite H. eexists ; repeat split. simpl. apply lt_IZR. rewrite abs_IZR. rewrite <- scaled_mantissa_generic with (1 := H). rewrite <- scaled_mantissa_abs. apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp (Rabs x))). apply bpow_gt_0. rewrite scaled_mantissa_mult_bpow. rewrite IZR_Zpower, <- bpow_plus. 2: now apply Zlt_le_weak. unfold cexp, FLX_exp. ring_simplify (prec + (mag beta (Rabs x) - prec))%Z. rewrite mag_abs. destruct (Req_dec x 0) as [Hx|Hx]. rewrite Hx, Rabs_R0. apply bpow_gt_0. destruct (mag beta x) as (ex, Ex). now apply Ex. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE