Let x0 of type ι be given.
Apply SNoS_E2 with
ordsucc omega,
x0,
∃ x1 . and (x1 ∈ omega) (SNoLt (abs_SNo (mul_SNo (eps_ x1) x0)) 1) leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H0.
Apply SNoLt_trichotomy_or_impred with
0,
x0,
∃ x1 . and (x1 ∈ omega) (SNoLt (abs_SNo (mul_SNo (eps_ x1) x0)) 1) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H5.
Apply SNoS_ordsucc_omega_bdd_eps_pos with
x0,
∃ x1 . and (x1 ∈ omega) (SNoLt (abs_SNo (mul_SNo (eps_ x1) x0)) 1) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Apply H8 with
∃ x2 . and (x2 ∈ omega) (SNoLt (abs_SNo (mul_SNo (eps_ x2) x0)) 1).
Apply mul_SNo_pos_pos with
eps_ x1,
x0 leaving 4 subgoals.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H9.
The subproof is completed by applying H5.
Apply SNo_eps_pos with
x1.
The subproof is completed by applying H9.
The subproof is completed by applying H7.
Let x2 of type ο be given.
Apply H12 with
x1.
Apply andI with
x1 ∈ omega,
SNoLt (abs_SNo (mul_SNo (eps_ x1) x0)) 1 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply pos_abs_SNo with
mul_SNo (eps_ x1) x0,
λ x3 x4 . SNoLt x4 1 leaving 2 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying H10.
Assume H7: 0 = x0.
Let x1 of type ο be given.
Apply H8 with
0.
Apply andI with
0 ∈ omega,
SNoLt (abs_SNo (mul_SNo (eps_ 0) x0)) 1 leaving 2 subgoals.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply H7 with
λ x2 x3 . SNoLt (abs_SNo (mul_SNo (eps_ 0) x2)) 1.
Apply mul_SNo_zeroR with
eps_ 0,
λ x2 x3 . SNoLt (abs_SNo x3) 1 leaving 2 subgoals.
Apply SNo_eps_ with
0.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply abs_SNo_0 with
λ x2 x3 . SNoLt x3 1.
The subproof is completed by applying SNoLt_0_1.
Apply SNoS_ordsucc_omega_bdd_eps_pos with
minus_SNo x0,
∃ x1 . and (x1 ∈ omega) (SNoLt (abs_SNo (mul_SNo (eps_ x1) x0)) 1) leaving 4 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
Let x1 of type ι be given.