proposition: Lemma contains_connected : forall xi, connected (fun x => contains xi (Xreal x)).
proof: Proof. intros [|l u] a b Ha Hb x Hx. exact I. split. destruct l as [|l]. exact I. exact (Rle_trans _ _ _ (proj1 Ha) (proj1 Hx)). destruct u as [|u]. exact I. exact (Rle_trans _ _ _ (proj2 Hx) (proj2 Hb)). Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic