∀ {α : Type u_1} {β : α → Type u_2} (l r : Std.DTreeMap.Internal.Impl α β),
  3 * 0 ≤
          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 ≤ 0 ∨
      (0 + (l.size + 1 + r.size + 1 + 0 + 1) ≤ 1 ∨
          0 ≤ 3 * (l.size + 1 + r.size + 1 + 0 + 1) ∧ l.size + 1 + r.size + 1 + 0 + 1 ≤ 3 * 0) ∨
        0 + (l.size + 1 + r.size + 1 + 0) ≤ 1 ∨
          0 ≤ 3 * (l.size + 1 + r.size + 1 + 0) ∧ l.size + 1 + r.size + 1 + 0 ≤ 3 * 0 →
    False