proposition: Theorem frexp_equiv : forall x : float, let (m, e) := Z.frexp x in (Prim2B m, e) = Bfrexp (Prim2B x).
proof: Proof. intro x. generalize (Z_frexp_spec x). destruct Z.frexp as [f e]. rewrite <-(B2SF_Prim2B x). replace (SFfrexp _ _ _) with (let (f, e) := Bfrexp (Prim2B x) in (B2SF f, e)). - case Bfrexp; intros f' e' [= H ->]; f_equal. now apply B2SF_inj; rewrite B2SF_Prim2B. - case (Prim2B x) as [s|s| |s m e' Hme] ; try easy. simpl. rewrite B2SF_SF2B. unfold Ffrexp_core_binary. change (digits2_pos m) with (Digits.digits2_pos m). now destruct Pos.leb. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN