proposition: Lemma le'_correct : forall x y, le' x y = true -> match F.toX x, F.toX y with | Xreal xr, Xreal yr => (xr <= yr)%R | _, _ => False end.
proof: Proof. intros x y. unfold le'. rewrite cmp_correct. destruct F.toX as [|xr]. easy. destruct F.toX as [|yr]. easy. simpl. now case Raux.Rcompare_spec ; auto with real. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic