Let x be given.

Assume Hx.

rewrite the current goal using exp_SNo_nat_S x Hx 1 nat_1 (from left to right).

We will prove x * x ^ 1 = x * x.

Use f_equal.

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

∎