Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply SNoLe_tra with
mul_SNo x0 x2,
mul_SNo x0 x3,
mul_SNo x1 x3 leaving 5 subgoals.
Apply SNo_mul_SNo with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply SNo_mul_SNo with
x0,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply SNo_mul_SNo with
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply nonneg_mul_SNo_Le with
x0,
x2,
x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H7.
Apply mul_SNo_com with
x0,
x3,
λ x4 x5 . SNoLe x5 (mul_SNo x1 x3) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply mul_SNo_com with
x1,
x3,
λ x4 x5 . SNoLe (mul_SNo x3 x0) x5 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply nonneg_mul_SNo_Le with
x3,
x0,
x1 leaving 5 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H6.