proposition: Theorem abs_B2R_lt_emax : forall x, (Rabs (B2R x) < bpow radix2 emax)%R.
proof: Proof. intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ). rewrite <- F2R_Zabs, abs_cond_Zopp. now apply bounded_lt_emax. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative