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