feat: add DTreeMap/TreeMap/TreeSet iterators and slices

src/Std/Data/DTreeMap.lean

@@ -9,3 +9,5 @@ prelude
 public import Std.Data.DTreeMap.Basic
 public import Std.Data.DTreeMap.AdditionalOperations
 public import Std.Data.DTreeMap.Lemmas
+public import Std.Data.DTreeMap.Iterator
+public import Std.Data.DTreeMap.Slice

src/Std/Data/DTreeMap/Internal/Def.lean

@@ -78,4 +78,11 @@ def toListModel : Impl α β → List ((a : α) × β a)
 @[simp] theorem toListModel_inner {sz k v l r} :
   (.inner sz k v l r : Impl α β).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel := rfl
 
+/--
+  Computes the size of the tree. Used for verification of iterators.
+-/
+def treeSize : Internal.Impl α β → Nat
+  | .leaf => 0
+  | .inner _ _ _ l r => 1 + l.treeSize + treeSize r
+
 end Std.DTreeMap.Internal.Impl

src/Std/Data/DTreeMap/Internal/Operations.lean

@@ -512,6 +512,10 @@ def insertMany! [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Imp
     r := ⟨r.val.insert! a b, fun h₀ h₁ => h₁ _ _ _ (r.2 h₀ h₁)⟩
   return r
 
+/-!
+## Operations for verification of iterators and slices
+-/
+
 namespace Const
 
 variable {β : Type v}