proposition: Lemma B2FF_BSN2B' : forall x Nx, B2FF (BSN2B' x Nx) = SF2FF (BinarySingleNaN.B2SF x).
proof: Proof. now intros [sx|sx| |sx mx ex Bx] Nx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN