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.
∎