∀ {α : Type u_1} {β : α → Type u_2} (sz : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
  (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) (newL : Std.DTreeMap.Internal.Impl α β)
  (h₁ : newL.Balanced) (h₂ : l.size - 1 ≤ newL.size) (h₃ : newL.size ≤ l.size + 1),
  (Std.DTreeMap.Internal.Impl.inner sz ky y l r).size - 1 ≤ (Std.DTreeMap.Internal.Impl.balance ky y newL r ⋯ ⋯ ⋯).size