rw [pow_zero, pow_zero, pow_zero]
a b : Nat
⊢ (a + b) ^ zero * (a + b) * (a + b) = a ^ zero * a * a + b ^ zero * b * b + succ (succ zero) * a * b
a b : Nat
⊢ one * (a + b) * (a + b) = one * a * a + one * b * b + succ (succ zero) * a * b