Let z be given.

Assume Hz.

rewrite the current goal using CD_exp_nat_S z 0 nat_0 (from left to right).

We will prove z ⨯ z ^ 0 = z.

rewrite the current goal using CD_exp_nat_0 z (from left to right).

We will prove z ⨯ 1 = z.

An exact proof term for the current goal is CD_mul_1R minus conj add mul F_0 F_1 F_minus_0 F_conj_0 F_conj_1 F_add_0L F_add_0R F_mul_0L F_mul_1R z Hz.

∎