proposition: Lemma contains_lower : forall l u x, contains (Ibnd (Xreal l) u) x -> contains (Ibnd (Xreal l) u) (Xreal l).
proof: Proof. intros. split. apply Rle_refl. destruct x as [|x]. elim H. destruct u as [|u]. exact I. apply Rle_trans with (1 := proj1 H) (2 := proj2 H). Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic