rewrite the current goal using exp_SNo_nat_1 2 SNo_2 (from right to left).

An exact proof term for the current goal is recip_SNo_pos_pow_2 1 nat_1.

∎