proposition: Theorem whole_correct : forall x, contains (convert whole) (Xreal x).
proof: Proof. intros x. simpl. rewrite F'.nan_correct. now rewrite F'.valid_lb_nan, F'.valid_ub_nan. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval