proposition: Theorem frshiftexp_equiv : forall x : float, let (m, e) := frshiftexp x in (Prim2B m, (to_Z e - shift)%Z) = Bfrexp (Prim2B x).
proof: Proof. intro x. generalize (frexp_equiv x). unfold Z.frexp. now case frshiftexp. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN