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.