proposition: Theorem of_int63_equiv : forall i, Prim2B (of_int63 i) = binary_normalize prec emax Hprec Hmax mode_NE (to_Z i) 0 false.
proof: Proof. intro i. apply B2SF_inj. rewrite B2SF_Prim2B. rewrite of_int63_spec. apply binary_normalize_equiv. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN