proposition: Theorem bounded_canonical_lt_emax : forall mx ex, canonical radix2 fexp (Float radix2 (Zpos mx) ex) -> (F2R (Float radix2 (Zpos mx) ex) < bpow radix2 emax)%R -> bounded mx ex = true.
proof: Proof. intros mx ex Cx Bx. apply andb_true_intro. split. unfold canonical_mantissa. unfold canonical, Fexp in Cx. rewrite Cx at 2. rewrite Zpos_digits2_pos. unfold cexp. rewrite mag_F2R_Zdigits. 2: discriminate. now apply -> Zeq_is_eq_bool. apply Zle_bool_true. unfold canonical, Fexp in Cx. rewrite Cx. unfold cexp, fexp, FLT_exp. destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). simpl. apply Z.max_lub. cut (e' - 1 < emax)%Z. clear ; lia. apply lt_bpow with radix2. apply Rle_lt_trans with (2 := Bx). change (Zpos mx) with (Z.abs (Zpos mx)). rewrite F2R_Zabs. apply Ex. apply Rgt_not_eq. now apply F2R_gt_0. apply Z.max_l_iff, fexp_emax. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative