proposition: Theorem build_nan_correct : forall x : { x | is_nan x = true }, build_nan x = proj1_sig x.
proof: Proof. intros [x H]. now destruct x. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN