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