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