Let n be given.

Assume Hn.

We prove the intermediate claim Len1: SNo (eps_ n).

An exact proof term for the current goal is SNo_eps_ n (nat_p_omega n Hn).

We prove the intermediate claim Len2: 0 < eps_ n.

An exact proof term for the current goal is SNo_eps_pos n (nat_p_omega n Hn).

We prove the intermediate claim Len3: eps_ n ≠ 0.

Assume H1: eps_ n = 0.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

rewrite the current goal using H1 (from right to left) at position 2.

We will prove 0 < eps_ n.

An exact proof term for the current goal is Len2.

Apply mul_SNo_nonzero_cancel (eps_ n) (recip_SNo_pos (eps_ n)) (2 ^ n) Len1 Len3 (SNo_recip_SNo_pos (eps_ n) Len1 Len2) (SNo_exp_SNo_nat 2 SNo_2 n Hn) to the current goal.

We will prove eps_ n * recip_SNo_pos (eps_ n) = eps_ n * 2 ^ n.

rewrite the current goal using mul_SNo_eps_power_2 n Hn (from left to right).

We will prove eps_ n * recip_SNo_pos (eps_ n) = 1.

An exact proof term for the current goal is recip_SNo_pos_invR (eps_ n) Len1 Len2.

∎