no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b
rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
  add_eq_zero_iff_eq_neg]