proposition: Lemma is_nan_correct : forall f, is_nan f = match classify f with Fnan => true | _ => false end.
proof: Proof. now intro f; case f. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig