We will prove div_SNo 1 2 = eps_ 1.

We prove the intermediate claim Hpos2: 0 < 2.

An exact proof term for the current goal is SNoLt_0_2.

We prove the intermediate claim HdivDef: div_SNo 1 2 = mul_SNo 1 (recip_SNo 2).

Use reflexivity.

rewrite the current goal using HdivDef (from left to right).

rewrite the current goal using (recip_SNo_poscase 2 Hpos2) (from left to right).

rewrite the current goal using recip_SNo_pos_2 (from left to right).

An exact proof term for the current goal is (mul_SNo_oneL (eps_ 1) SNo_eps_1).

∎