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