From d2b27035aebff082d83a3bcb20e9b9fd0afd0da9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Nov 2017 17:24:37 -0800
Subject: [PATCH] feat(library/init/data/rbtree/lemmas): add contains_correct
 user lemma

---
 library/init/data/rbtree/lemmas.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/library/init/data/rbtree/lemmas.lean b/library/init/data/rbtree/lemmas.lean
index 03885ff6fb..756a261876 100644
--- a/library/init/data/rbtree/lemmas.lean
+++ b/library/init/data/rbtree/lemmas.lean
@@ -541,4 +541,13 @@ variables {α : Type u} {lt : α → α → Prop} [decidable_rel lt]
 lemma mem_insert [is_irrefl α lt] : ∀ (a : α) (t : rbtree α lt), a ∈ t.insert a
 | a ⟨t, _⟩ := t.mem_insert lt a
 
+lemma contains_correct [is_strict_weak_order α lt] (a : α) (t : rbtree α lt) : a ∈ t ↔ (t.contains a = tt) :=
+begin
+  cases t,
+  simp [has_mem.mem, rbtree.mem, contains],
+  apply rbnode.contains_correct,
+  apply rbnode.is_searchable_of_well_formed,
+  assumption
+end
+
 end rbtree