proposition: Lemma toX_spec : forall x, toX_prop x (F.toX x).
proof: Proof. intros x. case_eq (F.toX x). intros _. apply toX_Xnan. intros r H. change r with (proj_val (Xreal r)). rewrite <- H. apply toX_Xreal. unfold F.toR. now rewrite H at 2. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic