Let x be given.

Assume Hx.

rewrite the current goal using exp_SNo_nat_S x Hx 0 nat_0 (from left to right).

We will prove x * x ^ 0 = x.

rewrite the current goal using exp_SNo_nat_0 x Hx (from left to right).

We will prove x * 1 = x.

An exact proof term for the current goal is mul_SNo_oneR x Hx.

∎