lean_workbook_plus_22968

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_22968 {r s R : ℝ} (h₁ : r ≥ 0 ∧ s ≥ 0 ∧ R ≥ 0) (h₂ : r ≤ s) (h₃ : s ≤ R + r) (h₄ : R ≤ s + r) : 16 * r ^ 2 * s ^ 2 * (3 * r ^ 2 - s ^ 2 + 4 * R * r + 4 * R ^ 2) ≥ 0   :=  by sorry