Let x be given.
Assume Hx Hx1.
Apply nat_ind to the current goal.
We will prove 1 ≤ x ^ 0.
rewrite the current goal using exp_SNo_nat_0 x Hx (from left to right).
Apply SNoLe_ref to the current goal.
Let n be given.
Assume Hn.
Assume IHn: 1 ≤ x ^ n.
We prove the intermediate claim Lxn: SNo (x ^ n).
An exact proof term for the current goal is SNo_exp_SNo_nat x Hx n Hn.
We will prove 1 ≤ x ^ (ordsucc n).
rewrite the current goal using exp_SNo_nat_S x Hx n Hn (from left to right).
We will prove 1 ≤ x * x ^ n.
rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from right to left).
We will prove 1 * 1 ≤ x * x ^ n.
Apply nonneg_mul_SNo_Le2 1 1 x (x ^ n) SNo_1 SNo_1 Hx Lxn to the current goal.
We will prove 0 ≤ 1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_1.
We will prove 0 ≤ 1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_1.
We will prove 1 ≤ x.
An exact proof term for the current goal is Hx1.
We will prove 1 ≤ x ^ n.
An exact proof term for the current goal is IHn.
∎