Let x, y and z be given.
Assume Hx Hy Hz H1.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy Hz.
Apply mul_SNo_nonzero_cancel 2 x (eps_ 1 * (y + z)) SNo_2 neq_2_0 Hx (SNo_mul_SNo (eps_ 1) (y + z) (SNo_eps_ 1 (nat_p_omega 1 nat_1)) Lyz) to the current goal.
We will prove 2 * x = 2 * eps_ 1 * (y + z).
rewrite the current goal using mul_SNo_assoc 2 (eps_ 1) (y + z) SNo_2 (SNo_eps_ 1 (nat_p_omega 1 nat_1)) Lyz (from left to right).
We will prove 2 * x = (2 * eps_ 1) * (y + z).
rewrite the current goal using eps_1_half_eq2 (from left to right).
We will prove 2 * x = 1 * (y + z).
rewrite the current goal using mul_SNo_oneL (y + z) Lyz (from left to right).
We will prove 2 * x = y + z.
rewrite the current goal using add_SNo_1_1_2 (from right to left).
We will prove (1 + 1) * x = y + z.
rewrite the current goal using mul_SNo_distrR 1 1 x SNo_1 SNo_1 Hx (from left to right).
We will prove 1 * x + 1 * x = y + z.
rewrite the current goal using mul_SNo_oneL x Hx (from left to right).
We will prove x + x = y + z.
An exact proof term for the current goal is H1.
∎