∀ {α : Type u_1} {β : Type u_2} (k : α) (sz : ℕ) (k' : α) (v' : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β),
  (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced →
    ∀ (v : β),
      (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').size - 1 ≤ (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size