proposition: Theorem normfr_mantissa_equiv : forall x, to_Z (normfr_mantissa x) = Z.of_N (Bnormfr_mantissa (Prim2B x)).
proof: Proof. intro x. rewrite normfr_mantissa_spec. rewrite <-B2SF_Prim2B. now case Prim2B. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN