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