We will prove 0 < x ^ 0.

rewrite the current goal using exp_SNo_nat_0 x Hx (from left to right).

We will prove 0 < 1.

An exact proof term for the current goal is SNoLt_0_1.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: 0 < x ^ n.

We will prove 0 < x ^ (ordsucc n).

rewrite the current goal using exp_SNo_nat_S x Hx n Hn (from left to right).

We will prove 0 < x * x ^ n.

rewrite the current goal using mul_SNo_zeroR x Hx (from right to left).

We will prove x * 0 < x * x ^ n.

An exact proof term for the current goal is pos_mul_SNo_Lt x 0 (x ^ n) Hx Hxpos SNo_0 (SNo_exp_SNo_nat x Hx n Hn) IHn.