Let x0 of type ι be given.
Apply not_nonneg_abs_SNo with
x0.
Apply SNoLt_irref with
x0.
Apply SNoLtLe_tra with
x0,
0,
x0 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.