Let n be given.

rewrite the current goal using exp_nat_S n 0 nat_0 (from left to right).

We will prove n * n ^ 0 = n.

rewrite the current goal using exp_nat_0 n (from left to right).

We will prove n * 1 = n.

Apply mul_nat_1R to the current goal.

∎