Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply mul_SNo_oneR with
x0,
λ x3 x4 . SNoLt (mul_SNo x2 x1) x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply recip_SNo_invL with
x1,
λ x3 x4 . SNoLt (mul_SNo x2 x1) (mul_SNo x0 x3) leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H5: x1 = 0.
Apply SNoLt_irref with
x1.
Apply H5 with
λ x3 x4 . SNoLt x4 x1.
The subproof is completed by applying H3.
Apply mul_SNo_assoc with
x0,
recip_SNo x1,
x1,
λ x3 x4 . SNoLt (mul_SNo x2 x1) x4 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply SNo_recip_SNo with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
Apply pos_mul_SNo_Lt' with
x2,
div_SNo x0 x1,
x1 leaving 5 subgoals.
The subproof is completed by applying H2.
Apply SNo_div_SNo with
x0,
x1 leaving 2 subgoals.
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 H3.
The subproof is completed by applying H4.