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
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + c * a - a * b * c = a * b + b * c + a * c * (1 - b)
no goals