proposition: Theorem bounded_lt_emax : forall mx ex, bounded mx ex = true -> (F2R (Float radix2 (Zpos mx) ex) < bpow radix2 emax)%R.
proof: Proof. intros mx ex Hx. destruct (andb_prop _ _ Hx) as (H1,H2). generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1. generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2. generalize (mag_F2R_Zdigits radix2 (Zpos mx) ex). destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). unfold mag_val. intros H. apply Rlt_le_trans with (bpow radix2 e'). change (Zpos mx) with (Z.abs (Zpos mx)). rewrite F2R_Zabs. apply Ex. apply Rgt_not_eq. now apply F2R_gt_0. apply bpow_le. rewrite H. 2: discriminate. revert H1. clear -H2. rewrite Zpos_digits2_pos. unfold fexp, FLT_exp. intros ; lia. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative