ring_nf
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
⊢ a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2 = b ^ 2 + c ^ 2 + a * b * c
no goals