Let x be given.
Assume Hx.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is nat_p_SNo x Hx.
Apply nat_ind to the current goal.
We will prove nat_p (x ^ 0).
rewrite the current goal using exp_SNo_nat_0 x Lx (from left to right).
An exact proof term for the current goal is nat_1.
Let n be given.
Assume Hn.
Assume IHn: nat_p (x ^ n).
We will prove nat_p (x ^ (ordsucc n)).
rewrite the current goal using exp_SNo_nat_S x Lx n Hn (from left to right).
We will prove nat_p (x * x ^ n).
rewrite the current goal using mul_nat_mul_SNo x (nat_p_omega x Hx) (x ^ n) (nat_p_omega (x ^ n) IHn) (from right to left).
We will prove nat_p (mul_nat x (x ^ n)).
An exact proof term for the current goal is mul_nat_p x Hx (x ^ n) IHn.
∎