Let x be given.

Assume Hx.

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

An exact proof term for the current goal is SNo_zero_or_sqr_pos x Hx.

∎