proposition: Lemma real_correct : forall x, F.real x = true -> F.toX x = Xreal (F.toR x).
proof: Proof. intros x Rx. rewrite F.real_correct in Rx. unfold F.toR. now destruct F.toX as [|rx]. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic