Apply nat_ind with λ x0 . ∀ x1 . or (atleastp x1 x0) (atleastp (ordsucc x0) x1) leaving 2 subgoals.

Let x0 of type ι be given.

Apply Empty_or_ex with x0, or (atleastp x0 0) (atleastp 1 x0) leaving 2 subgoals.

Assume H0: x0 = 0.

Apply orIL with atleastp x0 0, atleastp 1 x0.

Apply H0 with λ x1 x2 . atleastp x2 0.

The subproof is completed by applying unknownprop_b7030c4d179dca75b1c0a5a2dab6748493aebd2d7f37d4cf7a0d3bf2081224c9 with 0.

Assume H0: ∃ x1 . x1 ∈ x0.

Apply H0 with or (atleastp x0 0) (atleastp 1 x0).

Let x1 of type ι be given.

Assume H1: x1 ∈ x0.

Apply orIR with atleastp x0 0, atleastp 1 x0.

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι . inj u1 x0 x3 ⟶ x2.

Apply H2 with λ x3 . x1.

Apply andI with ∀ x3 . x3 ∈ u1 ⟶ x1 ∈ x0, ∀ x3 . x3 ∈ u1 ⟶ ∀ x4 . x4 ∈ u1 ⟶ x1 = x1 ⟶ x3 = x4 leaving 2 subgoals.

Let x3 of type ι be given.

Assume H3: x3 ∈ u1.

The subproof is completed by applying H1.

Let x3 of type ι be given.

Assume H3: x3 ∈ u1.

Let x4 of type ι be given.

Assume H4: x4 ∈ u1.

Assume H5: x1 = x1.

Apply cases_1 with x3, λ x5 . x5 = x4 leaving 2 subgoals.

The subproof is completed by applying H3.

Apply cases_1 with x4, λ x5 . 0 = x5 leaving 2 subgoals.

The subproof is completed by applying H4.

Let x5 of type ι → ι → ο be given.

Assume H6: x5 0 0.

The subproof is completed by applying H6.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . or (atleastp x1 x0) (atleastp (ordsucc x0) x1).

Let x1 of type ι be given.

Apply Empty_or_ex with x1, or (atleastp x1 (ordsucc x0)) (atleastp (ordsucc (ordsucc x0)) x1) leaving 2 subgoals.

Assume H2: x1 = 0.

Apply orIL with atleastp x1 (ordsucc x0), atleastp (ordsucc (ordsucc x0)) x1.

Apply H2 with λ x2 x3 . atleastp x3 (ordsucc x0).

The subproof is completed by applying unknownprop_b7030c4d179dca75b1c0a5a2dab6748493aebd2d7f37d4cf7a0d3bf2081224c9 with ordsucc x0.

Assume H2: ∃ x2 . x2 ∈ x1.

Apply H2 with or (atleastp x1 (ordsucc x0)) (atleastp (ordsucc (ordsucc x0)) x1).

Let x2 of type ι be given.

Assume H3: x2 ∈ x1.

Claim L4: ...

...

Claim L5: ...

...

Claim L6: ...

...

Apply H1 with setminus x1 (Sing x2), or (atleastp x1 (ordsucc x0)) (atleastp (ordsucc (ordsucc x0)) x1) leaving 2 subgoals.

Assume H7: atleastp (setminus x1 (Sing x2)) x0.

Apply orIL with atleastp x1 (ordsucc x0), atleastp (ordsucc (ordsucc x0)) x1.

Apply nat_setsum_ordsucc with x0, λ x3 x4 . atleastp x1 x3 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply L4 with λ x3 x4 . atleastp x3 (setsum 1 x0).

Apply unknownprop_94b237fc7b7d3bf1a0a078f7d057802d281bf3c46c36fd56a85d339ac0f07170 with Sing x2, setminus x1 (Sing x2), u1, x0 leaving 3 subgoals.

The subproof is completed by applying L6.

The subproof is completed by applying H7.

The subproof is completed by applying L5.

Assume H7: atleastp (ordsucc x0) (setminus x1 (Sing x2)).

Apply orIR with atleastp x1 (ordsucc x0), atleastp (ordsucc (ordsucc x0)) x1.

Apply nat_setsum_ordsucc with ordsucc x0, λ x3 x4 . atleastp x3 x1 leaving 2 subgoals.

Apply nat_ordsucc with x0.

The subproof is completed by applying H0.

Apply H7 with atleastp (setsum 1 (ordsucc x0)) ....

...

■

Proofgold Proof