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