Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_e8fe572c395c46aa7a6d67f7a8cd850bf647261d6b3677aecbf3b7ddfa5a7193 with
x0,
x1,
λ x3 x4 . SNoLt x3 (mul_CSNo x0 x2) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_e8fe572c395c46aa7a6d67f7a8cd850bf647261d6b3677aecbf3b7ddfa5a7193 with
x0,
x2,
λ x3 x4 . SNoLt (mul_SNo x0 x1) x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply pos_mul_SNo_Lt with
x0,
x1,
x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.