rw [succ_mul, succ_mul, zero_mul, zero_add, add_mul]
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + succ (succ zero) * a * b
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + (a * b + a * b)