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