∀ {α : Type u_1} {β : α → Type u_2} (ls : ℕ) (ll lr : Std.DTreeMap.Internal.Impl α β) (ls lls : ℕ)
  (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrl lrr : Std.DTreeMap.Internal.Impl α β),
  2 * (lrl.size + 1 + lrr.size) ≤ l.size + 1 + r.size →
    (l.Balanced ∧
          r.Balanced ∧ (l.size + r.size ≤ 1 ∨ l.size ≤ 3 * r.size ∧ r.size ≤ 3 * l.size) ∧ lls = l.size + 1 + r.size) ∧
        (lrl.Balanced ∧
            lrr.Balanced ∧
              (lrl.size + lrr.size ≤ 1 ∨ lrl.size ≤ 3 * lrr.size ∧ lrr.size ≤ 3 * lrl.size) ∧
                lrs = lrl.size + 1 + lrr.size) ∧
          (lls + lrs ≤ 1 ∨ lls ≤ 3 * lrs ∧ lrs ≤ 3 * lls) ∧ ls = lls + 1 + lrs →
      l.size + 1 + r.size < 2 * (lrl.size + 1 + lrr.size) → False