proposition: Theorem bounded_ge_emin : forall mx ex, bounded mx ex = true -> (bpow radix2 emin <= F2R (Float radix2 (Zpos mx) ex))%R.
proof: Proof. now apply bounded_ge_emin. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN