Let x0 of type ι be given.
Let x1 of type ι be given.
Apply SNoLt_trichotomy_or_impred with
x0,
x1,
x0 = x1 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply FalseE with
x0 = x1.
Apply SNoLt_irref with
mul_SNo x0 x0.
Apply H4 with
λ x2 x3 . SNoLt (mul_SNo x0 x0) x3.
Apply pos_mul_SNo_Lt2 with
x0,
x0,
x1,
x1 leaving 8 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 H2.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
The subproof is completed by applying H5.
Assume H5: x0 = x1.
The subproof is completed by applying H5.
Apply FalseE with
x0 = x1.
Apply SNoLt_irref with
mul_SNo x0 x0.
Apply H4 with
λ x2 x3 . SNoLt x3 (mul_SNo x0 x0).
Apply pos_mul_SNo_Lt2 with
x1,
x1,
x0,
x0 leaving 8 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H5.