proposition: Lemma cmp_correct : forall x y, cmp x y = match classify x, classify y with | Fnan, _ | _, Fnan => Xund | Fminfty, Fminfty => Xeq | Fminfty, _ => Xlt | _, Fminfty => Xgt | Fpinfty, Fpinfty => Xeq | _, Fpinfty => Xlt | Fpinfty, _ => Xgt | Freal, Freal => Xcmp (toX x) (toX y) end.
proof: Proof. intros x y. unfold cmp, classify. rewrite Fcmp_correct. now case x, y. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig