proposition: Theorem FLXN_format_generic : forall x, generic_format beta FLX_exp x -> FLXN_format x.
proof: Proof. intros x Hx. rewrite Hx. simpl. eexists. easy. rewrite <- Hx. intros Zx. simpl. split. apply le_IZR. rewrite IZR_Zpower. 2: now apply Zlt_0_le_0_pred. rewrite abs_IZR, <- scaled_mantissa_generic with (1 := Hx). apply Rmult_le_reg_r with (bpow (cexp beta FLX_exp x)). apply bpow_gt_0. rewrite <- bpow_plus. rewrite <- scaled_mantissa_abs. rewrite <- cexp_abs. rewrite scaled_mantissa_mult_bpow. unfold cexp, FLX_exp. rewrite mag_abs. ring_simplify (prec - 1 + (mag beta x - prec))%Z. destruct (mag beta x) as (ex,Ex). now apply Ex. apply lt_IZR. rewrite IZR_Zpower. 2: now apply Zlt_le_weak. rewrite abs_IZR, <- scaled_mantissa_generic with (1 := Hx). apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp x)). apply bpow_gt_0. rewrite <- bpow_plus. rewrite <- scaled_mantissa_abs. rewrite <- cexp_abs. rewrite scaled_mantissa_mult_bpow. unfold cexp, FLX_exp. rewrite mag_abs. ring_simplify (prec + (mag beta x - prec))%Z. 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