proposition: Theorem fromZ_correct : forall prec v, contains (convert (fromZ prec v)) (Xreal (IZR v)).
proof: Proof. intros. simpl. destruct (F.fromZ_DN_correct prec v) as [Hlv Lv]. destruct (F.fromZ_UP_correct prec v) as [Huv Uv]. rewrite Hlv, Huv. now apply le_contains. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval