proposition: Theorem abs_B2R_lt_emax : forall x, (Rabs (B2R x) < bpow radix2 emax)%R.
proof: Proof. intros x. rewrite <- B2R_B2BSN. now apply abs_B2R_lt_emax. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN