Search for blocks/addresses/...
Proofgold Proof
pf
Apply minus_SNo_minus_CSNo with
0
,
λ x0 x1 .
x0
=
0
leaving 2 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying minus_SNo_0.
■