∀ {α : Type u_1} {β : α → Type u_2} (ll lr l r : Std.DTreeMap.Internal.Impl α β),
  3 * (ll.size + 1 + lr.size) < l.size + 1 + r.size + 1 + 0 →
    3 * (ll.size + 1 + lr.size) ≤
            3 * 3 * (l.size + 1 + r.size + 1 + 0) + 3 * (l.size + 1 + r.size + 1 + 0) + (l.size + 1 + r.size + 1 + 0) +
              3 ∧
          l.size + 1 + r.size + 1 + 0 + 1 ≤ ll.size + 1 + lr.size ∨
        (ll.size + 1 + lr.size + (l.size + 1 + r.size + 1 + 0 + 1) ≤ 1 ∨
            ll.size + 1 + lr.size ≤ 3 * (l.size + 1 + r.size + 1 + 0 + 1) ∧
              l.size + 1 + r.size + 1 + 0 + 1 ≤ 3 * (ll.size + 1 + lr.size)) ∨
          ll.size + 1 + lr.size + (l.size + 1 + r.size + 1 + 0) ≤ 1 ∨
            ll.size + 1 + lr.size ≤ 3 * (l.size + 1 + r.size + 1 + 0) ∧
              l.size + 1 + r.size + 1 + 0 ≤ 3 * (ll.size + 1 + lr.size) →
      False