proposition: Theorem Bfrexp_correct : forall f, is_finite_strict f = true -> let x := B2R f in let z := fst (Bfrexp f) in let e := snd (Bfrexp f) in (/2 <= Rabs (B2R z) < 1)%R /\ (x = B2R z * bpow radix2 e)%R /\ e = mag radix2 x.
proof: Proof. intros x Fx. rewrite <- is_finite_strict_B2BSN in Fx. generalize (Bfrexp_correct prec emax _ (B2BSN x) Fx). simpl. rewrite <- B2R_B2BSN. rewrite B2BSN_lift. destruct BinarySingleNaN.Bfrexp as [z e]. rewrite B2R_B2BSN. now intros [H1 [H2 H3]]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN