Search for blocks/addresses/...
Proofgold Proof
pf
Apply unknownprop_483ab2c4cf352794c6e764ca83196651bc5de6ef598ec843402a4c02baafb47b 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.
■