proposition: Lemma is_nan_correct : forall f, is_nan f = match classify f with Sig.Fnan => true | _ => false end.
proof: Proof. now intro f; unfold is_nan, classify; case PrimFloat.classify. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig