Theorem: Nat.exp_succ (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
⊢ exp (n + 1) = 2 * exp n
Tactic:
simp [exp_def, pow_succ, mul_comm]
State after:
no goals