proposition: Lemma cmp_correct : forall x y, cmp x y = Xcmp (F.toX x) (F.toX y).
proof: Proof. intros x y. unfold cmp. rewrite !F.classify_correct, F.cmp_correct. generalize (F.classify_correct x). generalize (F.classify_correct y). rewrite !F.real_correct. now case (F.classify x), (F.classify y), (F.toX x), (F.toX y). Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic