Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
even_nat (add_SNo x1 (minus_SNo x0)).
Assume H4:
∀ x2 . x2 ∈ omega ⟶ x0 = mul_nat 2 x2 ⟶ ∀ x3 : ο . x3.
Apply H1 with
even_nat (add_SNo x1 (minus_SNo x0)).
Assume H6:
∀ x2 . x2 ∈ omega ⟶ x1 = mul_nat 2 x2 ⟶ ∀ x3 : ο . x3.
Apply omega_SNo with
x0.
The subproof is completed by applying H3.
Apply omega_SNo with
x1.
The subproof is completed by applying H5.
Apply unknownprop_17e526dd107b435f5416528d1c977ef8aa1ea06ba09d8b9ed0ca53424a454f1a with
add_SNo x1 (minus_SNo x0) leaving 2 subgoals.
Apply int_add_SNo with
x1,
minus_SNo x0 leaving 2 subgoals.
Apply nat_p_int with
x1.
Apply omega_nat_p with
x1.
The subproof is completed by applying H5.
Apply int_minus_SNo with
x0.
Apply nat_p_int with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H3.
Apply add_SNo_minus_Le2b with
x1,
x0,
0 leaving 4 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L7.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with
x0,
λ x2 x3 . SNoLe x3 x1 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying H2.
Apply unknownprop_d528c711b690b408e267d5af5f579a6a575d751567ba690169e9696970ff7ca9 with
x0,
add_SNo x1 (minus_SNo x0),
even_nat (add_SNo x1 (minus_SNo x0)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L9.
Apply H10 with
even_nat (add_SNo x1 (minus_SNo x0)).
Apply H13.
Apply add_nat_add_SNo with
x0,
add_SNo x1 (minus_SNo x0),
λ x2 x3 . odd_nat x3 leaving 3 subgoals.
The subproof is completed by applying H3.
Apply nat_p_omega with
add_SNo x1 (minus_SNo x0).
The subproof is completed by applying L9.
Apply add_SNo_com with
x1,
minus_SNo x0,
λ x2 x3 . odd_nat (add_SNo x0 x3) leaving 3 subgoals.
The subproof is completed by applying L8.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying L7.
Apply add_SNo_minus_SNo_prop2 with
x0,
x1,
λ x2 x3 . odd_nat x3 leaving 3 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
The subproof is completed by applying H1.