Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
The subproof is completed by applying If_i_1 with
SNoLt
0
x0
,
recip_SNo_pos
x0
,
If_i
(
SNoLt
x0
0
)
(
minus_SNo
(
recip_SNo_pos
(
minus_SNo
x0
)
)
)
0
.
■