Let x0 of type ι be given.
Let x1 of type ι be given.
Apply add_SNo_0R with
0,
λ x2 x3 . SNoLt (mul_SNo x0 x1) x2 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with
mul_SNo x0 x1,
λ x2 x3 . SNoLt x2 (add_SNo 0 0) leaving 2 subgoals.
Apply SNo_mul_SNo with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply mul_SNo_zeroR with
x1,
λ x2 x3 . SNoLt (add_SNo 0 (mul_SNo x0 x1)) (add_SNo 0 x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply mul_SNo_zeroR with
x0,
λ x2 x3 . SNoLt (add_SNo 0 (mul_SNo x0 x1)) (add_SNo x2 (mul_SNo x1 0)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply mul_SNo_zeroR with
0,
λ x2 x3 . SNoLt (add_SNo x2 (mul_SNo x0 x1)) (add_SNo (mul_SNo x0 0) (mul_SNo x1 0)) leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply mul_SNo_com with
x1,
0,
λ x2 x3 . SNoLt (add_SNo (mul_SNo 0 0) (mul_SNo x0 x1)) (add_SNo (mul_SNo x0 0) x3) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying SNo_0.
Apply mul_SNo_Lt with
x0,
0,
0,
x1 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.