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

We will prove (1 + 1) * eps_ 1 = 1.

rewrite the current goal using mul_SNo_distrR 1 1 (eps_ 1) SNo_1 SNo_1 SNo_eps_1 (from left to right).

We will prove 1 * eps_ 1 + 1 * eps_ 1 = 1.

rewrite the current goal using mul_SNo_oneL (eps_ 1) SNo_eps_1 (from left to right).

An exact proof term for the current goal is eps_1_half_eq1.

∎