Let x0 of type ι be given.
Apply add_SNo_com with
mul_SNo 2 x0,
1,
λ x1 x2 . odd_nat x2 leaving 3 subgoals.
Apply SNo_mul_SNo with
2,
x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply omega_SNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply odd_nat_1p2x with
x0.
The subproof is completed by applying H0.