proposition: Lemma real_correct : forall xi, real xi = match convert xi with Interval.Inan => false | _ => true end.
proof: Proof. now intros [|xl xu]; [|simpl; case (_ && _)]. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval