Search for blocks/addresses/...

Proofgold Proof

pf
Apply recip_SNo_poscase with 1, λ x0 x1 . x1 = 1 leaving 2 subgoals.
The subproof is completed by applying SNoLt_0_1.
The subproof is completed by applying recip_SNo_pos_1.