Theorem: Imo2012P4.sub_sq'' (Compfiles/Imo2012P4.lean)

State before:
x y : ℤ
⊢ x ^ 2 + y ^ 2 = 2 * x * y ↔ x = y
Tactic:
rw [← sub_eq_zero, ← sub_sq', sq_eq_zero_iff, sub_eq_zero]
State after:
no goals