proposition: Theorem abs_B2R_le_emax_minus_prec : forall x, (Rabs (B2R x) <= bpow radix2 emax - bpow radix2 (emax - prec))%R.
proof: Proof. intros [sx|sx| |sx mx ex Hx] ; simpl ; [rewrite Rabs_R0 ; apply Rle_0_minus, bpow_le ; revert prec_gt_0_; unfold Prec_gt_0; lia..|]. rewrite <- F2R_Zabs, abs_cond_Zopp. now apply bounded_le_emax_minus_prec. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative