Search for blocks/addresses/...

Proofgold Proof

pf
Apply If_i_0 with SNoLt 0 0, recip_SNo_pos 0, If_i (SNoLt 0 0) (minus_SNo (recip_SNo_pos (minus_SNo 0))) 0, λ x0 x1 . x1 = 0 leaving 2 subgoals.
The subproof is completed by applying SNoLt_irref with 0.
Apply If_i_0 with SNoLt 0 0, minus_SNo (recip_SNo_pos (minus_SNo 0)), 0.
The subproof is completed by applying SNoLt_irref with 0.