Let x0 of type ι be given.
Assume H1: x0 = 0 ⟶ ∀ x1 : ο . x1.
Apply nat_ind with
λ x1 . ∃ x2 . and (x2 ∈ int) (and (SNoLe (mul_SNo 2 (abs_SNo x2)) x0) (divides_nat x0 (add_SNo x1 (minus_SNo x2)))) leaving 2 subgoals.
Let x1 of type ο be given.
Apply H3 with
0.
Apply andI with
0 ∈ int,
and (SNoLe (mul_SNo 2 (abs_SNo 0)) x0) (divides_nat x0 (add_SNo 0 (minus_SNo 0))) leaving 2 subgoals.
Apply nat_p_int with
0.
The subproof is completed by applying nat_0.
Apply andI with
SNoLe (mul_SNo 2 (abs_SNo 0)) x0,
divides_nat x0 (add_SNo 0 (minus_SNo 0)) leaving 2 subgoals.
Apply abs_SNo_0 with
λ x2 x3 . SNoLe (mul_SNo 2 x3) x0.
Apply mul_SNo_zeroR with
2,
λ x2 x3 . SNoLe x3 x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply unknownprop_72fc13f59561a486e7f04b4e6ad6c40ec1d48eeac6e68c47cb50fa618c19e933 with
x0.
The subproof is completed by applying H0.
Apply minus_SNo_0 with
λ x2 x3 . divides_nat x0 (add_SNo 0 x3).
Apply add_SNo_0L with
0,
λ x2 x3 . divides_nat x0 x3 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply unknownprop_94b9b73b1207350973a964cfd79fac000c8d717e12b3149994867d613d318c69 with
x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.