Search for blocks/addresses/...

Proofgold Proof

pf
Apply mul_SNo_nonzero_cancel with 1, recip_SNo_pos 1, 1 leaving 5 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying neq_1_0.
Apply SNo_recip_SNo_pos with 1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNoLt_0_1.
The subproof is completed by applying SNo_1.
Apply mul_SNo_oneL with 1, λ x0 x1 . mul_SNo 1 (recip_SNo_pos 1) = x1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply recip_SNo_pos_invR with 1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNoLt_0_1.