lean_workbook_plus_37261
ProvedThe sum of four real numbers is and the sum of their squares is . Prove that these numbers can be denoted by so that holds.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37261 (a b c d : ℝ) (h₁ : a + b + c + d = 9) (h₂ : a^2 + b^2 + c^2 + d^2 = 21) : ∃ a b c d : ℝ, a + b + c + d = 9 ∧ a^2 + b^2 + c^2 + d^2 = 21 ∧ a * b - c * d ≥ 2 := by sorry
Source