Let x0 of type ι be given.
Apply mul_SNo_oneR with
eps_ x0,
λ x1 x2 . SNoLe x1 1 leaving 2 subgoals.
Apply SNo_eps_ with
x0.
The subproof is completed by applying H0.
Apply mul_SNo_eps_power_2 with
x0,
λ x1 x2 . SNoLe (mul_SNo (eps_ x0) 1) x1 leaving 2 subgoals.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Apply nonneg_mul_SNo_Le with
eps_ x0,
1,
exp_SNo_nat 2 x0 leaving 5 subgoals.
Apply SNo_eps_ with
x0.
The subproof is completed by applying H0.
Apply SNoLtLe with
0,
eps_ x0.
Apply SNo_eps_pos with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply SNo_exp_SNo_nat with
2,
x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Apply exp_SNo_1_bd with
2,
x0 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
Apply SNoLtLe with
1,
2.
The subproof is completed by applying SNoLt_1_2.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.