proposition: Theorem bounded_le_emax_minus_prec : forall mx ex, bounded mx ex = true -> (F2R (Float radix2 (Zpos mx) ex) <= bpow radix2 emax - bpow radix2 (emax - prec))%R.
proof: Proof. clear prec_lt_emax_. intros mx ex Hx. apply Rle_trans with ((bpow radix2 (Zdigits radix2 (Z.pos mx)) - 1) * bpow radix2 ex)%R. - apply Rmult_le_compat_r. apply bpow_ge_0. rewrite <- IZR_Zpower by apply Zdigits_ge_0. rewrite <- minus_IZR. apply IZR_le. apply Z.lt_le_pred. rewrite <- (Z.abs_eq (Z.pos mx)) by easy. apply Zdigits_correct. - destruct (andb_prop _ _ Hx) as [H1 H2]. apply Rle_trans with (bpow radix2 (ex + prec) - bpow radix2 ex)%R. { rewrite Rmult_minus_distr_r, Rmult_1_l, <- bpow_plus. apply Rplus_le_compat_r. apply bpow_le. apply Zeq_bool_eq in H1. rewrite Zpos_digits2_pos in H1. unfold fexp, FLT_exp in H1. clear -H1 ; lia. } replace emax with (emax - prec - ex + (ex + prec))%Z at 1 by ring. replace (emax - prec)%Z with (emax - prec - ex + ex)%Z at 2 by ring. do 2 rewrite (bpow_plus _ (emax - prec - ex)). rewrite <- Rmult_minus_distr_l. rewrite <- (Rmult_1_l (_ - _)) at 1. apply Rmult_le_compat_r. + apply Rle_0_minus, bpow_le. unfold Prec_gt_0 in prec_gt_0_. clear -prec_gt_0_ ; lia. + apply (bpow_le radix2 0). apply Zle_minus_le_0. now apply Zle_bool_imp_le. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative