have eq1 := calc
  (2 + a) * (2 - a) = 4 - a ^ 2 := by ring_nf
  _ = a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2 := by rw [h]
  _ = (b ^ 2 + c ^ 2) + a * b * c := by ring_nf
  _ ≥ 2 * b * c + a * b * c := by rel [two_mul_le_add_sq b c]
  _ = (2 + a) * (b * c) := by 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 * b + b * c + c * a - a * b * c ≤ 2
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)
⊢ a * b + b * c + c * a - a * b * c ≤ 2