Let z be given.
Assume Hz.
Apply nat_ind to the current goal.
rewrite the current goal using CD_exp_nat_0 (from left to right).
We will prove CD_carr 1.
An exact proof term for the current goal is CD_carr_0ext F_0 1 F_1.
Let n be given.
Assume Hn.
Assume IHn: CD_carr (z ^ n).
rewrite the current goal using CD_exp_nat_S z n Hn (from left to right).
We will prove CD_carr (z ⨯ z ^ n).
Apply CD_mul_CD minus conj add mul F_minus F_conj F_add F_mul to the current goal.
We will prove CD_carr z.
An exact proof term for the current goal is Hz.
We will prove CD_carr (z ^ n).
An exact proof term for the current goal is IHn.
∎