Search for blocks/addresses/...
Proofgold Proof
pf
Apply mul_SNo_com with
eps_
1
,
2
,
λ x0 x1 .
x1
=
1
leaving 3 subgoals.
The subproof is completed by applying SNo_eps_1.
The subproof is completed by applying SNo_2.
The subproof is completed by applying eps_1_half_eq2.
■