Let n be given.

Assume Hn.

We prove the intermediate claim L1: 0 < 2 ^ n.

An exact proof term for the current goal is exp_SNo_nat_pos 2 SNo_2 SNoLt_0_2 n Hn.

rewrite the current goal using recip_SNo_poscase (2 ^ n) L1 (from left to right).

An exact proof term for the current goal is recip_SNo_pos_pow_2 n Hn.

∎