proposition: Lemma generic_format_fexp_IZR : forall n prec emax, (0 < prec)%Z -> (3 - prec < emax)%Z -> (Z.abs n <= 2 ^ prec)%Z -> generic_format radix2 (fexp prec emax) (IZR n).
proof: Proof. intros n prec emax Hprec Hemax H. apply generic_format_abs_inv. rewrite <-abs_IZR. apply generic_format_FLT. unfold SpecFloat.emin. apply Zle_lt_or_eq in H. destruct H as [H | H]. - now apply (FLT_spec _ _ _ _ (Float radix2 (Z.abs n) 0)); [unfold F2R; simpl; rewrite Rmult_1_r |simpl; rewrite Z.abs_involutive |simpl Fexp; lia]. - rewrite H. now apply (FLT_spec _ _ _ _ (Float radix2 1 prec)); [unfold F2R; simpl; rewrite Rmult_1_l; destruct prec |simpl Fnum; apply Zpower_gt_1 |simpl Fexp; lia]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)