proposition: Lemma not_empty_contains : forall xi x, contains xi x -> not_empty xi.
proof: Proof. intros xi x Hx. exists (proj_val x). now apply contains_Xreal. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic