proposition: Theorem is_nan_Bfrexp : forall x, is_nan (fst (Bfrexp x)) = is_nan x.
proof: Proof. intros [sx|sx| |sx mx ex Bx] ; try easy. simpl. rewrite is_nan_SF2B. unfold Ffrexp_core_binary. destruct Zlt_bool ; try easy. now destruct Pos.leb. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative