rel [two_mul_le_add_sq b c]
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ b ^ 2 + c ^ 2 + a * b * c ≥ 2 * b * c + a * b * c
no goals