lean_workbook_plus_65043

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_65043 : ∀ a b c : ℝ, (a + 1) / (b ^ 2 + 1) + (b + 1) / (c ^ 2 + 1) + (c + 1) / (a ^ 2 + 1) ≤ a ^ 2 + b ^ 2 + c ^ 2   :=  by sorry