proposition: Lemma nan_correct : F.toX F.nan = Xnan.
proof: Proof. generalize (F.classify_correct F.nan). generalize F.nan_correct. case F.classify; [easy|intros _|easy..]. generalize (F.real_correct F.nan). now case F.toX; [|intros r H; rewrite H]. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic