Let x0 of type ι be given.
Apply setminusE with
omega,
Sing 0,
x0,
∀ x1 . nat_p x1 ⟶ divides_int x0 (add_SNo x1 (minus_SNo (96eca.. x0 x1))) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply nat_ind with
λ x1 . divides_int x0 (add_SNo x1 (minus_SNo (96eca.. x0 x1))) leaving 2 subgoals.
Apply unknownprop_32031505644b872a0911c2de665524637f3e933b5a278f213bfb34b1b7b14a8c with
x0,
λ x1 x2 . divides_int x0 (add_SNo 0 (minus_SNo x2)).
Apply minus_SNo_0 with
λ x1 x2 . divides_int x0 (add_SNo 0 x2).
Apply add_SNo_0L with
0,
λ x1 x2 . divides_int x0 x2 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply divides_int_0 with
x0.
Apply nat_p_int with
x0.
The subproof is completed by applying L3.
Let x1 of type ι be given.
Apply ordinal_ordsucc_SNo_eq with
x1,
λ x2 x3 . divides_int x0 (add_SNo x3 (minus_SNo (ordsucc (96eca.. x0 x1)))) leaving 2 subgoals.
Apply nat_p_ordinal with
x1.
The subproof is completed by applying H4.
Apply ordinal_ordsucc_SNo_eq with
96eca.. x0 x1,
λ x2 x3 . divides_int x0 (add_SNo (add_SNo 1 x1) (minus_SNo x3)) leaving 2 subgoals.
The subproof is completed by applying L7.
Apply minus_add_SNo_distr with
1,
96eca.. x0 x1,
λ x2 x3 . divides_int x0 (add_SNo (add_SNo 1 x1) x3) leaving 3 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L8.
Apply xm with
ordsucc (96eca.. x0 x1) ∈ x0,
divides_int x0 (add_SNo (ordsucc x1) (minus_SNo (96eca.. x0 (ordsucc x1)))) leaving 2 subgoals.
Apply unknownprop_0b6bf9289375e2fec7f133c86f85e21365e99b363c22a457be49ec227de43d5d with
x0,
x1,
λ x2 x3 . divides_int x0 (add_SNo (ordsucc x1) (minus_SNo x3)) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H10.
The subproof is completed by applying L9.
Apply unknownprop_5638b8a3f345573382122a22afd2c2865d379a7a354b4f08c0e6004c928d3e17 with
x0,
x1,
λ x2 x3 . divides_int x0 (add_SNo (ordsucc x1) (minus_SNo x3)) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H10.
Apply minus_SNo_0 with
λ x2 x3 . divides_int x0 (add_SNo (ordsucc x1) x3).
Apply add_SNo_0R with
ordsucc x1,
λ x2 x3 . divides_int x0 x3 leaving 2 subgoals.
The subproof is completed by applying L6.
Apply add_SNo_minus_R2' with
ordsucc x1,
x0,
λ x2 x3 . divides_int x0 x2 leaving 3 subgoals.
The subproof is completed by applying L6.
Apply nat_p_SNo with
x0.
The subproof is completed by applying L3.
Apply divides_int_add_SNo with
x0,
add_SNo (ordsucc x1) (minus_SNo x0),
x0 leaving 2 subgoals.
Apply ordinal_ordsucc_In_eq with
x0,
96eca.. x0 x1,
ordsucc (96eca.. x0 x1) = x0,
λ x2 x3 . divides_int x0 (add_SNo (ordsucc x1) (minus_SNo x2)) leaving 5 subgoals.
Apply nat_p_ordinal with
x0.
The subproof is completed by applying L3.
Apply unknownprop_b8495c15b713ede179e55ace8614d7c473b63e6d664fda42134df335ee990bdf with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply FalseE with
ordsucc (96eca.. x0 x1) = x0.
Apply H10.
The subproof is completed by applying H11.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H11 with λ x3 x4 . x2 x4 x3.
The subproof is completed by applying L9.
Apply divides_int_ref with
x0.
Apply nat_p_int with
x0.
The subproof is completed by applying L3.