Let x0 of type ι be given.
Apply nat_ind with
λ x1 . ∀ x2 x3 . atleastp (add_nat x0 x1) (binunion x2 x3) ⟶ or (atleastp x0 x2) (atleastp x1 x3) leaving 2 subgoals.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply add_nat_0R with
x0,
λ x3 x4 . atleastp x4 (binunion x1 x2) ⟶ or (atleastp x0 x1) (atleastp 0 x2).
Apply orIR with
atleastp x0 x1,
atleastp 0 x2.
The subproof is completed by applying unknownprop_b7030c4d179dca75b1c0a5a2dab6748493aebd2d7f37d4cf7a0d3bf2081224c9 with x2.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply add_nat_SR with
x0,
x1,
λ x4 x5 . atleastp x5 (binunion x2 x3) ⟶ or (atleastp x0 x2) (atleastp (ordsucc x1) x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H3 with
or (atleastp x0 x2) (atleastp (ordsucc x1) x3).
Let x4 of type ι → ι be given.
Apply H4 with
or (atleastp x0 x2) (atleastp (ordsucc x1) x3).
Apply xm with
∀ x5 . x5 ∈ x0 ⟶ x4 x5 ∈ x2,
or (atleastp x0 x2) (atleastp (ordsucc x1) x3) leaving 2 subgoals.
Assume H7: ∀ x5 . x5 ∈ x0 ⟶ x4 x5 ∈ x2.
Apply orIL with
atleastp x0 x2,
atleastp (ordsucc x1) x3.
Let x5 of type ο be given.
Assume H8:
∀ x6 : ι → ι . inj x0 x2 x6 ⟶ x5.
Apply H8 with
x4.
Apply andI with
∀ x6 . x6 ∈ x0 ⟶ x4 x6 ∈ x2,
∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 x6 = x4 x7 ⟶ x6 = x7 leaving 2 subgoals.
The subproof is completed by applying H7.
Let x6 of type ι be given.
Assume H9: x6 ∈ x0.
Let x7 of type ι be given.
Assume H10: x7 ∈ x0.
Apply H6 with
x6,
x7 leaving 2 subgoals.
Apply ordsuccI1 with
add_nat x0 x1,
x6.
Apply unknownprop_2dcf4dd8557a0ffd2a187961d1bc330ef1aae42c546555814bac26eb5e3c6d68 with
x0,
x1,
x6 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H9.
Apply ordsuccI1 with
add_nat x0 x1,
x7.
Apply unknownprop_2dcf4dd8557a0ffd2a187961d1bc330ef1aae42c546555814bac26eb5e3c6d68 with
x0,
x1,
x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H10.
Assume H7:
not (∀ x5 . x5 ∈ x0 ⟶ x4 x5 ∈ x2).