Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
even_nat (add_SNo x1 (minus_SNo x0)).
Apply H1 with
even_nat (add_SNo x1 (minus_SNo x0)).
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_4adaec41cb5534e7de6e9f2e22a12d61a97262a6e78399e6df58393eee854625 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 . even_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 . even_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 . even_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.