Let x be given.
Assume Hx.
Apply nat_ind to the current goal.
We will prove SNo (x ^ 0).
rewrite the current goal using exp_SNo_nat_0 x Hx (from left to right).
An exact proof term for the current goal is SNo_1.
Let n be given.
Assume Hn.
Assume IHn: SNo (x ^ n).
We will prove SNo (x ^ (ordsucc n)).
rewrite the current goal using exp_SNo_nat_S x Hx n Hn (from left to right).
We will prove SNo (x * x ^ n).
An exact proof term for the current goal is SNo_mul_SNo x (x ^ n) Hx IHn.
∎