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
.
■