Let x0 of type ι be given.
Apply SNoLt_trichotomy_or_impred with
x0,
0,
or (x0 = 0) (SNoLt 0 (mul_SNo x0 x0)) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Apply orIR with
x0 = 0,
SNoLt 0 (mul_SNo x0 x0).
Apply mul_SNo_neg_neg with
x0,
x0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying orIL with
x0 = 0,
SNoLt 0 (mul_SNo x0 x0).
Apply orIR with
x0 = 0,
SNoLt 0 (mul_SNo x0 x0).
Apply mul_SNo_pos_pos with
x0,
x0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H1.