AMC_2021_A_7.lean

import data.real.basic


theorem AMC_2021_A_7 (x y:ℝ): (x*y-1)^2+(x+y)^2≥1:=
begin
  sorry
end