refactor(library): rbtree lemmas do not need to be in init folder

library/data/rbtree/default.lean

@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import data.rbtree.lemmas

library/data/rbtree/lemmas.lean

@@ -1,11 +1,8 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
-prelude
-import init.data.rbtree.basic init.meta init.data.nat
-
 universes u v
 
 /- TODO(Leo): remove after we cleanup stdlib simp lemmas -/

library/init/data/rbtree/basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 prelude
 import init.data.ordering

library/init/data/rbtree/default.lean

@@ -1,10 +1,10 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 prelude
-import init.data.rbtree.basic init.data.rbtree.lemmas
+import init.data.rbtree.basic
 
 meta def rbtree.default_lt : tactic unit :=
 `[apply has_lt.lt]