Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2:
not (and (x0 = 0) (x1 = 0)).
Apply least_ordinal_ex with
λ x2 . and (int_lin_comb x0 x1 x2) (SNoLt 0 x2),
∃ x2 . and (and (int_lin_comb x0 x1 x2) (SNoLt 0 x2)) (∀ x3 . int_lin_comb x0 x1 x3 ⟶ SNoLt 0 x3 ⟶ SNoLe x2 x3) leaving 2 subgoals.
Apply int_3_cases with
x0,
∃ x2 . and (ordinal x2) ((λ x3 . and (int_lin_comb x0 x1 x3) (SNoLt 0 x3)) x2) leaving 4 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Let x3 of type ο be given.
Apply H9 with
ordsucc x2.
Apply andI with
ordinal (ordsucc x2),
(λ x4 . and (int_lin_comb x0 x1 x4) (SNoLt 0 x4)) (ordsucc x2) leaving 2 subgoals.
Apply ordinal_ordsucc with
x2.
Apply nat_p_ordinal with
x2.
The subproof is completed by applying L7.
Apply andI with
int_lin_comb x0 x1 (ordsucc x2),
SNoLt 0 (ordsucc x2) leaving 2 subgoals.
Apply int_lin_comb_I with
x0,
x1,
ordsucc x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply Subq_omega_int with
ordsucc x2.
Apply omega_ordsucc with
x2.
The subproof is completed by applying H5.
Let x4 of type ο be given.
Apply H10 with
minus_SNo 1.
Apply andI with
minus_SNo 1 ∈ int,
∃ x5 . and (x5 ∈ int) (add_SNo (mul_SNo (minus_SNo 1) x0) (mul_SNo x5 x1) = ordsucc x2) leaving 2 subgoals.
Apply int_minus_SNo_omega with
1.
Apply nat_p_omega with
1.
The subproof is completed by applying nat_1.
Let x5 of type ο be given.
Apply H11 with
0.
Apply andI with
0 ∈ int,
add_SNo (mul_SNo (minus_SNo 1) x0) (mul_SNo 0 x1) = ordsucc x2 leaving 2 subgoals.
Apply Subq_omega_int with
0.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply mul_SNo_zeroL with
x1,
λ x6 x7 . add_SNo (mul_SNo (minus_SNo 1) x0) x7 = ordsucc x2 leaving 2 subgoals.
The subproof is completed by applying L4.
Apply mul_SNo_minus_distrL with
1,
x0,
λ x6 x7 . add_SNo x7 0 = ordsucc x2 leaving 3 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L3.
Apply mul_SNo_oneL with
x0,
λ x6 x7 . add_SNo (minus_SNo x7) 0 = ordsucc x2 leaving 2 subgoals.
The subproof is completed by applying L3.
Apply H6 with
λ x6 x7 . add_SNo (minus_SNo x7) 0 = ordsucc x2.
Apply minus_SNo_invol with
ordsucc x2,
λ x6 x7 . add_SNo x7 0 = ordsucc x2 leaving 2 subgoals.
The subproof is completed by applying L8.
Apply add_SNo_0R with
ordsucc x2.
The subproof is completed by applying L8.
Apply ordinal_ordsucc_pos with
x2.
Apply nat_p_ordinal with
x2.
The subproof is completed by applying L7.