Let n be given.
Assume Hn.
Apply nat_ind to the current goal.
We will prove nat_p (n ^ 0).
rewrite the current goal using exp_nat_0 (from left to right).
An exact proof term for the current goal is nat_1.
Let m be given.
Assume Hm IHm.
We will prove nat_p (n ^ ordsucc m).
rewrite the current goal using exp_nat_S n m Hm (from left to right).
We will prove nat_p (n * n ^ m).
An exact proof term for the current goal is mul_nat_p n Hn (n ^ m) IHm.
∎