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