Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2: 0 ∈ x0.
Assume H3: 1 ∈ x1.
Apply nat_p_ordinal with
x0.
The subproof is completed by applying H0.
Apply nat_p_ordinal with
x1.
The subproof is completed by applying H1.
Apply ordinal_SNo with
x0.
The subproof is completed by applying L4.
Apply ordinal_SNo with
x1.
The subproof is completed by applying L5.
Apply ordinal_In_SNoLt with
x0,
0 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
Apply ordinal_In_SNoLt with
x1,
1 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H3.
Apply ordinal_SNoLt_In with
x0,
mul_nat x0 x1 leaving 3 subgoals.
The subproof is completed by applying L4.
Apply nat_p_ordinal with
mul_nat x0 x1.
Apply mul_nat_p with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply mul_nat_mul_SNo with
x0,
x1,
λ x2 x3 . SNoLt x0 x3 leaving 3 subgoals.
Apply nat_p_omega with
x0.
The subproof is completed by applying H0.
Apply nat_p_omega with
x1.
The subproof is completed by applying H1.
Apply add_SNo_0L with
x0,
λ x2 x3 . SNoLt x2 (mul_SNo x0 x1) leaving 2 subgoals.
The subproof is completed by applying L6.
Apply add_SNo_minus_Lt2 with
mul_SNo x0 x1,
x0,
0 leaving 4 subgoals.
Apply SNo_mul_SNo with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L6.
The subproof is completed by applying SNo_0.
Apply mul_SNo_oneR with
x0,
λ x2 x3 . SNoLt 0 (add_SNo (mul_SNo x0 x1) (minus_SNo x2)) leaving 2 subgoals.
The subproof is completed by applying L6.
Apply mul_SNo_minus_distrR with
x0,
1,
λ x2 x3 . SNoLt 0 (add_SNo (mul_SNo x0 x1) x2) leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying SNo_1.
Apply mul_SNo_distrL with
x0,
x1,
minus_SNo 1,
λ x2 x3 . SNoLt 0 x2 leaving 4 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
Apply SNo_minus_SNo with
1.
The subproof is completed by applying SNo_1.
Apply mul_SNo_pos_pos with
x0,
add_SNo x1 (minus_SNo 1) leaving 4 subgoals.
The subproof is completed by applying L6.
Apply SNo_add_SNo with
x1,
minus_SNo 1 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply SNo_minus_SNo with
1.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L8.
Apply add_SNo_minus_Lt2b with
x1,
1,
0 leaving 4 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with
1,
λ x2 x3 . SNoLt x3 x1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L9.