Let z be given.

Assume Hz.

rewrite the current goal using CD_exp_nat_S z 1 nat_1 (from left to right).

We will prove z ⨯ z ^ 1 = z ⨯ z.

Use f_equal.

An exact proof term for the current goal is CD_exp_nat_1 z Hz.

∎