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