simpa using by linarith
case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im
no goals