Search for blocks/addresses/...
Proofgold Proof
pf
Apply HSNo_OSNo with
Quaternion_j
.
The subproof is completed by applying HSNo_Quaternion_j.
■