Let x0 of type ι be given.
Apply If_i_0 with
SNoLt 0 x0,
recip_SNo_pos x0,
If_i (SNoLt x0 0) (minus_SNo (recip_SNo_pos (minus_SNo x0))) 0,
λ x1 x2 . x2 = minus_SNo (recip_SNo_pos (minus_SNo x0)) leaving 2 subgoals.
Apply SNoLt_irref with
0.
Apply SNoLt_tra with
0,
x0,
0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.