Search for blocks/addresses/...
Proofgold Proof
pf
Apply unknownprop_647ec341c7696352fb8a30f001c79d84c2767a0fc283d06b71b39a980b6ecefe with
SNo
,
add_SNo
,
mul_SNo
leaving 2 subgoals.
The subproof is completed by applying SNo_add_SNo.
The subproof is completed by applying mul_SNo_distrL.
■