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