Assume Hex: ∃m : set, nat_p m ∧ n = ordsucc m.

Apply Hex to the current goal.

Let m be given.

Assume Hmconj: nat_p m ∧ n = ordsucc m.

We prove the intermediate claim HmNat: nat_p m.

An exact proof term for the current goal is (andEL (nat_p m) (n = ordsucc m) Hmconj).

We prove the intermediate claim HnEq: n = ordsucc m.

An exact proof term for the current goal is (andER (nat_p m) (n = ordsucc m) Hmconj).

We prove the intermediate claim HmO: m ∈ ω.

An exact proof term for the current goal is (nat_p_omega m HmNat).

We prove the intermediate claim HnX: (1,n) ∈ X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 1 n In_1_2 HnO).

We prove the intermediate claim HsuccNO: ordsucc n ∈ ω.

An exact proof term for the current goal is (omega_ordsucc n HnO).

Set a to be the term (1,m).

Set b to be the term (1,ordsucc n).

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 1 m In_1_2 HmO).

We prove the intermediate claim HbX: b ∈ X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 1 (ordsucc n) In_1_2 HsuccNO).

Set U to be the term {y ∈ X|order_rel X a y ∧ order_rel X y b}.

We prove the intermediate claim HUpow: U ∈ 𝒫 X.

Apply PowerI X U to the current goal.

Let y be given.

Assume Hy: y ∈ U.

An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y Hy).

We prove the intermediate claim HUinB: U ∈ order_topology_basis X.

Set A to be the term {I ∈ 𝒫 X|∃a0 ∈ X, ∃b0 ∈ X, I = {y0 ∈ X|order_rel X a0 y0 ∧ order_rel X y0 b0}}.

Set B to be the term {I ∈ 𝒫 X|∃b0 ∈ X, I = {y0 ∈ X|order_rel X y0 b0}}.

Set C to be the term {I ∈ 𝒫 X|∃a0 ∈ X, I = {y0 ∈ X|order_rel X a0 y0}}.

Set Bold to be the term (A ∪ B ∪ C).

We prove the intermediate claim HUA: U ∈ A.

Apply (SepI (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, ∃b0 ∈ X, I = {y0 ∈ X|order_rel X a0 y0 ∧ order_rel X y0 b0}) U HUpow) to the current goal.

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaX.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbX.

Use reflexivity.

We prove the intermediate claim HUAB: U ∈ (A ∪ B).

An exact proof term for the current goal is (binunionI1 A B U HUA).

We prove the intermediate claim HUbold: U ∈ Bold.

An exact proof term for the current goal is (binunionI1 (A ∪ B) C U HUAB).

We prove the intermediate claim HUdef: order_topology_basis X = (Bold ∪ {X}).

Use reflexivity.

rewrite the current goal using HUdef (from left to right).

An exact proof term for the current goal is (binunionI1 Bold {X} U HUbold).

We prove the intermediate claim HUopen: U ∈ order_topology X.

An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) U HUpow HUinB).

We prove the intermediate claim HUeq: U = {(1,n)}.

Apply set_ext to the current goal.

Let y be given.

Assume HyU: y ∈ U.

We will prove y ∈ {(1,n)}.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y HyU).

We prove the intermediate claim Hya: order_rel X a y.

An exact proof term for the current goal is (andEL (order_rel X a y) (order_rel X y b) (SepE2 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y HyU)).

We prove the intermediate claim Hyb: order_rel X y b.

An exact proof term for the current goal is (andER (order_rel X a y) (order_rel X y b) (SepE2 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y HyU)).

We prove the intermediate claim Hso: simply_ordered_set X.

An exact proof term for the current goal is simply_ordered_set_setprod_2_omega.

Apply (order_rel_trichotomy_or_impred X y (1,n) Hso HyX HnX (y ∈ {(1,n)})) to the current goal.

Assume Hyln: order_rel X y (1,n).

Apply FalseE to the current goal.

We prove the intermediate claim HyUp: order_rel (setprod 2 ω) y (1,ordsucc m).

rewrite the current goal using HnEq (from right to left).

An exact proof term for the current goal is Hyln.

An exact proof term for the current goal is (no_point_between_setprod_2_omega_1n_1succn m y HmO HyX Hya HyUp).

Assume Hey: y = (1,n).

rewrite the current goal using Hey (from left to right).

An exact proof term for the current goal is (SingI (1,n)).

Assume Hnly: order_rel X (1,n) y.

Apply FalseE to the current goal.

An exact proof term for the current goal is (no_point_between_setprod_2_omega_1n_1succn n y HnO HyX Hnly Hyb).

Let y be given.

Assume HyS: y ∈ {(1,n)}.

We will prove y ∈ U.

We prove the intermediate claim Hey: y = (1,n).

An exact proof term for the current goal is (SingE (1,n) y HyS).

rewrite the current goal using Hey (from left to right).

We prove the intermediate claim Hrel1: order_rel (setprod 2 ω) a (1,n).

We will prove order_rel (setprod 2 ω) a (1,n).

rewrite the current goal using HnEq (from left to right).

Apply (order_rel_setprod_2_omega_intro 1 m 1 (ordsucc m) In_1_2 HmO In_1_2 (omega_ordsucc m HmO)) to the current goal.

Apply orIR to the current goal.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is (ordsuccI2 m).

We prove the intermediate claim Hrel2: order_rel (setprod 2 ω) (1,n) b.

We will prove order_rel (setprod 2 ω) (1,n) b.

Apply (order_rel_setprod_2_omega_intro 1 n 1 (ordsucc n) In_1_2 HnO In_1_2 (omega_ordsucc n HnO)) to the current goal.

Apply orIR to the current goal.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is (ordsuccI2 n).

Apply (SepI X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) (1,n) HnX) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hrel1.

An exact proof term for the current goal is Hrel2.

rewrite the current goal using HUeq (from right to left).

An exact proof term for the current goal is HUopen.