proposition: Theorem canonical_bounded : forall sx mx ex, bounded mx ex = true -> canonical radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex).
proof: Proof. intros sx mx ex H. apply canonical_canonical_mantissa. now apply andb_prop in H. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative