Apply mul_SNo_distrR with
1,
1,
eps_ 1,
λ x0 x1 . x1 = 1 leaving 4 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_eps_1.
Apply mul_SNo_oneL with
eps_ 1,
λ x0 x1 . add_SNo x1 x1 = 1 leaving 2 subgoals.
The subproof is completed by applying SNo_eps_1.
The subproof is completed by applying eps_1_half_eq1.