simp only [mul_comm]
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
⊢ a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
no goals