proposition: Lemma is_finite_BSN2B : forall nan x, is_finite (BSN2B nan x) = BinarySingleNaN.is_finite x.
proof: Proof. now intros nan [s|s| |s m e H]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN