proposition: Lemma le_correct : forall x y, F.toX x = Xreal (F.toR x) -> F.toX y = Xreal (F.toR y) -> le x y = Rle_bool (F.toR x) (F.toR y).
proof: Proof. intros x y Rx Ry. unfold le. rewrite F.cmp_correct. generalize (F.classify_correct x). generalize (F.classify_correct y). rewrite !F.real_correct, Rx, Ry. do 2 (case F.classify; [|easy..]; intros _). simpl. unfold Rle_bool. now case Rcompare. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic