We will prove atleastp (𝒫 ω) real.

Set L_ to be the term λX n ⇒ nat_primrec {0} (λn r ⇒ if n ∈ X then r ∪ {x + eps_ (ordsucc n)|x ∈ r} else r) n of type set → set → set.

Set R_ to be the term λX n ⇒ nat_primrec {1} (λn r ⇒ if n ∈ X then r else r ∪ {x + - eps_ (ordsucc n)|x ∈ r}) n of type set → set → set.

We prove the intermediate claim L_0: ∀X, L_ X 0 = {0}.

Let X be given.

An exact proof term for the current goal is nat_primrec_0 {0} (λn r ⇒ if n ∈ X then r ∪ {x + eps_ (ordsucc n)|x ∈ r} else r).

We prove the intermediate claim R_0: ∀X, R_ X 0 = {1}.

Let X be given.

An exact proof term for the current goal is nat_primrec_0 {1} (λn r ⇒ if n ∈ X then r else r ∪ {x + - eps_ (ordsucc n)|x ∈ r}).

We prove the intermediate claim L_ordsucc: ∀X, ∀n ∈ ω, L_ X (ordsucc n) = if n ∈ X then L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n} else L_ X n.

Let X and n be given.

Assume Hn.

An exact proof term for the current goal is nat_primrec_S {0} (λn r ⇒ if n ∈ X then r ∪ {x + eps_ (ordsucc n)|x ∈ r} else r) n (omega_nat_p n Hn).

We prove the intermediate claim R_ordsucc: ∀X, ∀n ∈ ω, R_ X (ordsucc n) = if n ∈ X then R_ X n else R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}.

Let X and n be given.

Assume Hn.

An exact proof term for the current goal is nat_primrec_S {1} (λn r ⇒ if n ∈ X then r else r ∪ {x + - eps_ (ordsucc n)|x ∈ r}) n (omega_nat_p n Hn).

We prove the intermediate claim L_ordsucc_pos: ∀X, ∀n ∈ ω, n ∈ X → L_ X (ordsucc n) = L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n}.

Let X and n be given.

Assume Hn HnX.

An exact proof term for the current goal is If_i_1 (n ∈ X) (L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n}) (L_ X n) HnX (λu _ ⇒ L_ X (ordsucc n) = u) (L_ordsucc X n Hn).

We prove the intermediate claim L_ordsucc_neg: ∀X, ∀n ∈ ω, n ∉ X → L_ X (ordsucc n) = L_ X n.

Let X and n be given.

Assume Hn HnX.

An exact proof term for the current goal is If_i_0 (n ∈ X) (L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n}) (L_ X n) HnX (λu _ ⇒ L_ X (ordsucc n) = u) (L_ordsucc X n Hn).

We prove the intermediate claim R_ordsucc_pos: ∀X, ∀n ∈ ω, n ∈ X → R_ X (ordsucc n) = R_ X n.

Let X and n be given.

Assume Hn HnX.

An exact proof term for the current goal is If_i_1 (n ∈ X) (R_ X n) (R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}) HnX (λu _ ⇒ R_ X (ordsucc n) = u) (R_ordsucc X n Hn).

We prove the intermediate claim R_ordsucc_neg: ∀X, ∀n ∈ ω, n ∉ X → R_ X (ordsucc n) = R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}.

Let X and n be given.

Assume Hn HnX.

An exact proof term for the current goal is If_i_0 (n ∈ X) (R_ X n) (R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}) HnX (λu _ ⇒ R_ X (ordsucc n) = u) (R_ordsucc X n Hn).

We prove the intermediate claim L_SNo1: ∀X, ∀n, nat_p n → ∀u ∈ L_ X n, SNo u.

Let X be given.

Apply nat_ind to the current goal.

We will prove ∀u ∈ L_ X 0, SNo u.

Apply L_0 X (λ_ v ⇒ ∀u ∈ v, SNo u) to the current goal.

Let u be given.

Assume Hu: u ∈ {0}.

rewrite the current goal using SingE 0 u Hu (from left to right).

We will prove SNo 0.

An exact proof term for the current goal is SNo_0.

Let n be given.

Assume Hn.

Assume IHn: ∀u ∈ L_ X n, SNo u.

We will prove ∀u ∈ L_ X (ordsucc n), SNo u.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply L_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ ∀u ∈ v, SNo u) to the current goal.

Let u be given.

Assume Hu: u ∈ L_ X n ∪ {w + eps_ (ordsucc n)|w ∈ L_ X n}.

Apply binunionE (L_ X n) {w + eps_ (ordsucc n)|w ∈ L_ X n} u Hu to the current goal.

An exact proof term for the current goal is IHn u.

Assume H2: u ∈ {w + eps_ (ordsucc n)|w ∈ L_ X n}.

Apply ReplE_impred (L_ X n) (λw ⇒ w + eps_ (ordsucc n)) u H2 to the current goal.

Let w be given.

Assume Hw: w ∈ L_ X n.

Assume Huw: u = w + eps_ (ordsucc n).

We will prove SNo u.

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

We will prove SNo (w + eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo w (eps_ (ordsucc n)) (IHn w Hw) (SNo_eps_ (ordsucc n) (omega_ordsucc n (nat_p_omega n Hn))).

Assume H1: n ∉ X.

Apply L_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ ∀u ∈ v, SNo u) to the current goal.

An exact proof term for the current goal is IHn.

We prove the intermediate claim R_SNo1: ∀X, ∀n, nat_p n → ∀u ∈ R_ X n, SNo u.

Let X be given.

Apply nat_ind to the current goal.

We will prove ∀u ∈ R_ X 0, SNo u.

Apply R_0 X (λ_ v ⇒ ∀u ∈ v, SNo u) to the current goal.

Let u be given.

Assume Hu: u ∈ {1}.

rewrite the current goal using SingE 1 u Hu (from left to right).

An exact proof term for the current goal is SNo_1.

Let n be given.

Assume Hn.

Assume IHn: ∀u ∈ R_ X n, SNo u.

We will prove ∀u ∈ R_ X (ordsucc n), SNo u.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply R_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ ∀u ∈ v, SNo u) to the current goal.

An exact proof term for the current goal is IHn.

Assume H1: n ∉ X.

Apply R_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ ∀u ∈ v, SNo u) to the current goal.

Let u be given.

Assume Hu: u ∈ R_ X n ∪ {w + - eps_ (ordsucc n)|w ∈ R_ X n}.

Apply binunionE (R_ X n) {w + - eps_ (ordsucc n)|w ∈ R_ X n} u Hu to the current goal.

An exact proof term for the current goal is IHn u.

Assume H2: u ∈ {w + - eps_ (ordsucc n)|w ∈ R_ X n}.

Apply ReplE_impred (R_ X n) (λw ⇒ w + - eps_ (ordsucc n)) u H2 to the current goal.

Let w be given.

Assume Hw: w ∈ R_ X n.

Assume Huw: u = w + - eps_ (ordsucc n).

We will prove SNo u.

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

We will prove SNo (w + - eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo w (- eps_ (ordsucc n)) (IHn w Hw) (SNo_minus_SNo (eps_ (ordsucc n)) (SNo_eps_ (ordsucc n) (omega_ordsucc n (nat_p_omega n Hn)))).

We prove the intermediate claim L_fin: ∀X, ∀n, nat_p n → finite (L_ X n).

Let X be given.

Apply nat_ind to the current goal.

We will prove finite (L_ X 0).

Apply L_0 X (λ_ v ⇒ finite v) to the current goal.

We will prove finite {0}.

Apply Sing_finite to the current goal.

Let n be given.

Assume Hn.

Assume IHn: finite (L_ X n).

We will prove finite (L_ X (ordsucc n)).

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply L_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ finite v) to the current goal.

We will prove finite (L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n}).

Apply binunion_finite to the current goal.

An exact proof term for the current goal is IHn.

We will prove finite {x + eps_ (ordsucc n)|x ∈ L_ X n}.

Apply Repl_finite to the current goal.

An exact proof term for the current goal is IHn.

Assume H1: n ∉ X.

Apply L_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ finite v) to the current goal.

An exact proof term for the current goal is IHn.

We prove the intermediate claim R_fin: ∀X, ∀n, nat_p n → finite (R_ X n).

Let X be given.

Apply nat_ind to the current goal.

We will prove finite (R_ X 0).

Apply R_0 X (λ_ v ⇒ finite v) to the current goal.

We will prove finite {1}.

Apply Sing_finite to the current goal.

Let n be given.

Assume Hn.

Assume IHn: finite (R_ X n).

We will prove finite (R_ X (ordsucc n)).

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply R_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ finite v) to the current goal.

An exact proof term for the current goal is IHn.

Assume H1: n ∉ X.

Apply R_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ finite v) to the current goal.

We will prove finite (R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}).

Apply binunion_finite to the current goal.

An exact proof term for the current goal is IHn.

We will prove finite {x + - eps_ (ordsucc n)|x ∈ R_ X n}.

Apply Repl_finite to the current goal.

An exact proof term for the current goal is IHn.

We prove the intermediate claim L_ordsucc_Subq: ∀X, ∀n, nat_p n → L_ X n ⊆ L_ X (ordsucc n).

Let X and n be given.

Assume Hn.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply L_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ L_ X n ⊆ v) to the current goal.

We will prove L_ X n ⊆ L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n}.

Apply binunion_Subq_1 to the current goal.

Assume H1: n ∉ X.

Apply L_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ L_ X n ⊆ v) to the current goal.

We will prove L_ X n ⊆ L_ X n.

Apply Subq_ref to the current goal.

We prove the intermediate claim R_ordsucc_Subq: ∀X, ∀n, nat_p n → R_ X n ⊆ R_ X (ordsucc n).

Let X and n be given.

Assume Hn.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply R_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ R_ X n ⊆ v) to the current goal.

We will prove R_ X n ⊆ R_ X n.

Apply Subq_ref to the current goal.

Assume H1: n ∉ X.

Apply R_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ R_ X n ⊆ v) to the current goal.

We will prove R_ X n ⊆ R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}.

Apply binunion_Subq_1 to the current goal.

We prove the intermediate claim L_Subq: ∀X, ∀n, nat_p n → ∀m ∈ n, L_ X m ⊆ L_ X n.

Let X be given.

Apply nat_ind to the current goal.

Let m be given.

Assume Hm: m ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE m Hm.

Let n be given.

Assume Hn.

Assume IHn: ∀m ∈ n, L_ X m ⊆ L_ X n.

Let m be given.

Assume Hm: m ∈ ordsucc n.

Apply ordsuccE n m Hm to the current goal.

Assume H1: m ∈ n.

We will prove L_ X m ⊆ L_ X (ordsucc n).

Apply Subq_tra (L_ X m) (L_ X n) (L_ X (ordsucc n)) to the current goal.

An exact proof term for the current goal is IHn m H1.

An exact proof term for the current goal is L_ordsucc_Subq X n Hn.

Assume H1: m = n.

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

An exact proof term for the current goal is L_ordsucc_Subq X n Hn.

We prove the intermediate claim R_Subq: ∀X, ∀n, nat_p n → ∀m ∈ n, R_ X m ⊆ R_ X n.

Let X be given.

Apply nat_ind to the current goal.

Let m be given.

Assume Hm: m ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE m Hm.

Let n be given.

Assume Hn.

Assume IHn: ∀m ∈ n, R_ X m ⊆ R_ X n.

Let m be given.

Assume Hm: m ∈ ordsucc n.

Apply ordsuccE n m Hm to the current goal.

Assume H1: m ∈ n.

We will prove R_ X m ⊆ R_ X (ordsucc n).

Apply Subq_tra (R_ X m) (R_ X n) (R_ X (ordsucc n)) to the current goal.

An exact proof term for the current goal is IHn m H1.

An exact proof term for the current goal is R_ordsucc_Subq X n Hn.

Assume H1: m = n.

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

An exact proof term for the current goal is R_ordsucc_Subq X n Hn.

We prove the intermediate claim L_0_In: ∀X, ∀n, nat_p n → 0 ∈ L_ X n.

Let X be given.

We prove the intermediate claim L_0_In_0: 0 ∈ L_ X 0.

An exact proof term for the current goal is L_0 X (λ_ v ⇒ 0 ∈ v) (SingI 0).

Apply nat_inv_impred to the current goal.

An exact proof term for the current goal is L_0_In_0.

Let n be given.

Assume Hn.

We will prove 0 ∈ L_ X (ordsucc n).

An exact proof term for the current goal is L_Subq X (ordsucc n) (nat_ordsucc n Hn) 0 (nat_0_in_ordsucc n Hn) 0 L_0_In_0.

We prove the intermediate claim R_1_In: ∀X, ∀n, nat_p n → 1 ∈ R_ X n.

Let X be given.

We prove the intermediate claim R_1_In_0: 1 ∈ R_ X 0.

An exact proof term for the current goal is R_0 X (λ_ v ⇒ 1 ∈ v) (SingI 1).

Apply nat_inv_impred to the current goal.

An exact proof term for the current goal is R_1_In_0.

Let n be given.

Assume Hn.

We will prove 1 ∈ R_ X (ordsucc n).

An exact proof term for the current goal is R_Subq X (ordsucc n) (nat_ordsucc n Hn) 0 (nat_0_in_ordsucc n Hn) 1 R_1_In_0.

We prove the intermediate claim L_ne: ∀X, ∀n, nat_p n → L_ X n ≠ 0.

Let X and n be given.

Assume Hn.

Assume H1: L_ X n = 0.

Apply EmptyE 0 to the current goal.

We will prove 0 ∈ 0.

rewrite the current goal using H1 (from right to left) at position 2.

An exact proof term for the current goal is L_0_In X n Hn.

We prove the intermediate claim R_ne: ∀X, ∀n, nat_p n → R_ X n ≠ 0.

Let X and n be given.

Assume Hn.

Assume H1: R_ X n = 0.

Apply EmptyE 1 to the current goal.

We will prove 1 ∈ 0.

rewrite the current goal using H1 (from right to left) at position 2.

An exact proof term for the current goal is R_1_In X n Hn.

We prove the intermediate claim L_R_dist: ∀X, ∀n, nat_p n → ∀w z, SNo_max_of (L_ X n) w → SNo_min_of (R_ X n) z → z = w + eps_ n.

Let X be given.

Apply nat_ind to the current goal.

Let w and z be given.

We will prove SNo_max_of (L_ X 0) w → SNo_min_of (R_ X 0) z → z = w + eps_ 0.

Apply L_0 X (λ_ v ⇒ SNo_max_of v w → SNo_min_of (R_ X 0) z → z = w + eps_ 0) to the current goal.

Assume Hw: SNo_max_of {0} w.

Apply R_0 X (λ_ v ⇒ SNo_min_of v z → z = w + eps_ 0) to the current goal.

Assume Hz: SNo_min_of {1} z.

Apply Hw to the current goal.

Assume H.

Apply H to the current goal.

Assume Hw1: w ∈ {0}.

Assume _ _.

Apply Hz to the current goal.

Assume H.

Apply H to the current goal.

Assume Hz1: z ∈ {1}.

Assume _ _.

rewrite the current goal using SingE 0 w Hw1 (from left to right).

rewrite the current goal using SingE 1 z Hz1 (from left to right).

We will prove 1 = 0 + eps_ 0.

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

Use symmetry.

An exact proof term for the current goal is add_SNo_0L 1 SNo_1.

Let n be given.

Assume Hn.

Assume IHn: ∀w z, SNo_max_of (L_ X n) w → SNo_min_of (R_ X n) z → z = w + eps_ n.

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

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

We prove the intermediate claim Len: SNo (eps_ n).

An exact proof term for the current goal is SNo_eps_ n (nat_p_omega n Hn).

We prove the intermediate claim LeSn: SNo (eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_eps_ (ordsucc n) LSn.

We prove the intermediate claim LmeSn: SNo (- eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_minus_SNo (eps_ (ordsucc n)) LeSn.

Let w and z be given.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply L_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ SNo_max_of v w → SNo_min_of (R_ X (ordsucc n)) z → z = w + eps_ (ordsucc n)) to the current goal.

Assume Hw: SNo_max_of (L_ X n ∪ {w + eps_ (ordsucc n)|w ∈ L_ X n}) w.

Apply R_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ SNo_min_of v z → z = w + eps_ (ordsucc n)) to the current goal.

Assume Hz: SNo_min_of (R_ X n) z.

Apply finite_max_exists (L_ X n) (L_SNo1 X n Hn) (L_fin X n Hn) (L_ne X n Hn) to the current goal.

Let w' be given.

Assume Hw': SNo_max_of (L_ X n) w'.

Apply Hw' to the current goal.

Assume H.

Apply H to the current goal.

Assume Hw'1: w' ∈ L_ X n.

Assume Hw'2: SNo w'.

Assume Hw'3: ∀y ∈ L_ X n, SNo y → y ≤ w'.

We prove the intermediate claim Lww': w = w' + eps_ (ordsucc n).

Apply Hw to the current goal.

Assume H.

Apply H to the current goal.

Assume Hw1: w ∈ L_ X n ∪ {w + eps_ (ordsucc n)|w ∈ L_ X n}.

Assume Hw2: SNo w.

Assume Hw3: ∀y ∈ L_ X n ∪ {w + eps_ (ordsucc n)|w ∈ L_ X n}, SNo y → y ≤ w.

Apply binunionE (L_ X n) {w + eps_ (ordsucc n)|w ∈ L_ X n} w Hw1 to the current goal.

Assume H2: w ∈ L_ X n.

We will prove False.

Apply SNoLt_irref w to the current goal.

We will prove w < w.

Apply SNoLtLe_tra w (w + eps_ (ordsucc n)) w Hw2 (SNo_add_SNo w (eps_ (ordsucc n)) Hw2 LeSn) Hw2 to the current goal.

We will prove w < w + eps_ (ordsucc n).

An exact proof term for the current goal is add_SNo_eps_Lt w Hw2 (ordsucc n) LSn.

We will prove w + eps_ (ordsucc n) ≤ w.

Apply Hw3 to the current goal.

We will prove w + eps_ (ordsucc n) ∈ L_ X n ∪ {w + eps_ (ordsucc n)|w ∈ L_ X n}.

Apply binunionI2 to the current goal.

We will prove w + eps_ (ordsucc n) ∈ {w + eps_ (ordsucc n)|w ∈ L_ X n}.

An exact proof term for the current goal is ReplI (L_ X n) (λw ⇒ w + eps_ (ordsucc n)) w H2.

We will prove SNo (w + eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo w (eps_ (ordsucc n)) Hw2 LeSn.

Assume H2: w ∈ {w + eps_ (ordsucc n)|w ∈ L_ X n}.

Apply ReplE_impred (L_ X n) (λw ⇒ w + eps_ (ordsucc n)) w H2 to the current goal.

Let w'' be given.

Assume Hw'': w'' ∈ L_ X n.

Assume Hww'': w = w'' + eps_ (ordsucc n).

We will prove w = w' + eps_ (ordsucc n).

We prove the intermediate claim Lw'': SNo w''.

An exact proof term for the current goal is L_SNo1 X n Hn w'' Hw''.

Apply SNoLe_antisym w (w' + eps_ (ordsucc n)) Hw2 (SNo_add_SNo w' (eps_ (ordsucc n)) Hw'2 LeSn) to the current goal.

We will prove w ≤ w' + eps_ (ordsucc n).

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

We will prove w'' + eps_ (ordsucc n) ≤ w' + eps_ (ordsucc n).

Apply add_SNo_Le1 w'' (eps_ (ordsucc n)) w' Lw'' LeSn Hw'2 to the current goal.

We will prove w'' ≤ w'.

Apply Hw'3 to the current goal.

We will prove w'' ∈ L_ X n.

An exact proof term for the current goal is Hw''.

We will prove SNo w''.

An exact proof term for the current goal is Lw''.

We will prove w' + eps_ (ordsucc n) ≤ w.

Apply Hw3 to the current goal.

We will prove w' + eps_ (ordsucc n) ∈ L_ X n ∪ {w + eps_ (ordsucc n)|w ∈ L_ X n}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI (L_ X n) (λw ⇒ w + eps_ (ordsucc n)) w' Hw'1.

We will prove SNo (w' + eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo w' (eps_ (ordsucc n)) Hw'2 LeSn.

We will prove z = w + eps_ (ordsucc n).

Use transitivity with w' + eps_ n, w' + eps_ (ordsucc n) + eps_ (ordsucc n), and (w' + eps_ (ordsucc n)) + eps_ (ordsucc n).

We will prove z = w' + eps_ n.

An exact proof term for the current goal is IHn w' z Hw' Hz.

We will prove w' + eps_ n = w' + eps_ (ordsucc n) + eps_ (ordsucc n).

Use f_equal.

Use symmetry.

An exact proof term for the current goal is eps_ordsucc_half_add n Hn.

We will prove w' + eps_ (ordsucc n) + eps_ (ordsucc n) = (w' + eps_ (ordsucc n)) + eps_ (ordsucc n).

An exact proof term for the current goal is add_SNo_assoc w' (eps_ (ordsucc n)) (eps_ (ordsucc n)) Hw'2 LeSn LeSn.

We will prove (w' + eps_ (ordsucc n)) + eps_ (ordsucc n) = w + eps_ (ordsucc n).

Use f_equal.

Use symmetry.

An exact proof term for the current goal is Lww'.

Assume H1: n ∉ X.

Apply L_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ SNo_max_of v w → SNo_min_of (R_ X (ordsucc n)) z → z = w + eps_ (ordsucc n)) to the current goal.

Assume Hw: SNo_max_of (L_ X n) w.

Apply R_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ SNo_min_of v z → z = w + eps_ (ordsucc n)) to the current goal.

Assume Hz: SNo_min_of (R_ X n ∪ {w + - eps_ (ordsucc n)|w ∈ R_ X n}) z.

Apply finite_min_exists (R_ X n) (R_SNo1 X n Hn) (R_fin X n Hn) (R_ne X n Hn) to the current goal.

Let z' be given.

Assume Hz': SNo_min_of (R_ X n) z'.

Apply Hz' to the current goal.

Assume H.

Apply H to the current goal.

Assume Hz'1: z' ∈ R_ X n.

Assume Hz'2: SNo z'.

Assume Hz'3: ∀y ∈ R_ X n, SNo y → z' ≤ y.

We prove the intermediate claim Lzz': z = z' + - eps_ (ordsucc n).

Apply Hz to the current goal.

Assume H.

Apply H to the current goal.

Assume Hz1: z ∈ R_ X n ∪ {z + - eps_ (ordsucc n)|z ∈ R_ X n}.

Assume Hz2: SNo z.

Assume Hz3: ∀y ∈ R_ X n ∪ {z + - eps_ (ordsucc n)|z ∈ R_ X n}, SNo y → z ≤ y.

Apply binunionE (R_ X n) {z + - eps_ (ordsucc n)|z ∈ R_ X n} z Hz1 to the current goal.

Assume H2: z ∈ R_ X n.

We will prove False.

Apply SNoLt_irref z to the current goal.

We will prove z < z.

Apply SNoLeLt_tra z (z + - eps_ (ordsucc n)) z Hz2 (SNo_add_SNo z (- eps_ (ordsucc n)) Hz2 LmeSn) Hz2 to the current goal.

We will prove z ≤ z + - eps_ (ordsucc n).

Apply Hz3 to the current goal.

We will prove z + - eps_ (ordsucc n) ∈ R_ X n ∪ {z + - eps_ (ordsucc n)|z ∈ R_ X n}.

Apply binunionI2 to the current goal.

We will prove z + - eps_ (ordsucc n) ∈ {z + - eps_ (ordsucc n)|z ∈ R_ X n}.

An exact proof term for the current goal is ReplI (R_ X n) (λz ⇒ z + - eps_ (ordsucc n)) z H2.

We will prove SNo (z + - eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo z (- eps_ (ordsucc n)) Hz2 LmeSn.

We will prove z + - eps_ (ordsucc n) < z.

rewrite the current goal using add_SNo_0R z Hz2 (from right to left) at position 2.

We will prove z + - eps_ (ordsucc n) < z + 0.

Apply add_SNo_Lt2 z (- eps_ (ordsucc n)) 0 Hz2 LmeSn SNo_0 to the current goal.

We will prove - eps_ (ordsucc n) < 0.

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

We will prove - eps_ (ordsucc n) < - 0.

An exact proof term for the current goal is minus_SNo_Lt_contra 0 (eps_ (ordsucc n)) SNo_0 LeSn (SNo_eps_pos (ordsucc n) (omega_ordsucc n (nat_p_omega n Hn))).

Assume H2: z ∈ {z + - eps_ (ordsucc n)|z ∈ R_ X n}.

Apply ReplE_impred (R_ X n) (λz ⇒ z + - eps_ (ordsucc n)) z H2 to the current goal.

Let z'' be given.

Assume Hz'': z'' ∈ R_ X n.

Assume Hzz'': z = z'' + - eps_ (ordsucc n).

We will prove z = z' + - eps_ (ordsucc n).

We prove the intermediate claim Lz'': SNo z''.

An exact proof term for the current goal is R_SNo1 X n Hn z'' Hz''.

Apply SNoLe_antisym z (z' + - eps_ (ordsucc n)) Hz2 (SNo_add_SNo z' (- eps_ (ordsucc n)) Hz'2 LmeSn) to the current goal.

We will prove z ≤ z' + - eps_ (ordsucc n).

Apply Hz3 to the current goal.

We will prove z' + - eps_ (ordsucc n) ∈ R_ X n ∪ {z + - eps_ (ordsucc n)|z ∈ R_ X n}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI (R_ X n) (λz ⇒ z + - eps_ (ordsucc n)) z' Hz'1.

We will prove SNo (z' + - eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo z' (- eps_ (ordsucc n)) Hz'2 LmeSn.

We will prove z' + - eps_ (ordsucc n) ≤ z.

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

We will prove z' + - eps_ (ordsucc n) ≤ z'' + - eps_ (ordsucc n).

Apply add_SNo_Le1 z' (- eps_ (ordsucc n)) z'' Hz'2 LmeSn Lz'' to the current goal.

We will prove z' ≤ z''.

Apply Hz'3 to the current goal.

We will prove z'' ∈ R_ X n.

An exact proof term for the current goal is Hz''.

We will prove SNo z''.

An exact proof term for the current goal is Lz''.

Apply Hw to the current goal.

Assume H.

Apply H to the current goal.

Assume Hw1: w ∈ L_ X n.

Assume Hw2: SNo w.

Assume Hw3: ∀y ∈ L_ X n, SNo y → y ≤ w.

We will prove z = w + eps_ (ordsucc n).

Use transitivity with z' + - eps_ (ordsucc n), (w + eps_ n) + - eps_ (ordsucc n), and w + (eps_ n + - eps_ (ordsucc n)).

An exact proof term for the current goal is Lzz'.

Use f_equal.

An exact proof term for the current goal is IHn w z' Hw Hz'.

We will prove (w + eps_ n) + - eps_ (ordsucc n) = w + (eps_ n + - eps_ (ordsucc n)).

Use symmetry.

An exact proof term for the current goal is add_SNo_assoc w (eps_ n) (- eps_ (ordsucc n)) Hw2 Len LmeSn.

Use f_equal.

We will prove eps_ n + - eps_ (ordsucc n) = eps_ (ordsucc n).

rewrite the current goal using eps_ordsucc_half_add n Hn (from right to left).

An exact proof term for the current goal is add_SNo_minus_R2 (eps_ (ordsucc n)) (eps_ (ordsucc n)) LeSn LeSn.

We prove the intermediate claim L_SNo: ∀X, ∀n, nat_p n → L_ X n ⊆ SNoS_ ω.

Let X be given.

Apply nat_ind to the current goal.

We will prove L_ X 0 ⊆ SNoS_ ω.

Apply L_0 X (λ_ v ⇒ v ⊆ SNoS_ ω) to the current goal.

We will prove {0} ⊆ SNoS_ ω.

Let u be given.

Assume Hu.

rewrite the current goal using SingE 0 u Hu (from left to right).

We will prove 0 ∈ SNoS_ ω.

Apply SNoS_I ω omega_ordinal 0 0 (nat_p_omega 0 nat_0) to the current goal.

We will prove SNo_ 0 0.

An exact proof term for the current goal is ordinal_SNo_ Empty ordinal_Empty.

Let n be given.

Assume Hn.

Assume IHn: L_ X n ⊆ SNoS_ ω.

We will prove L_ X (ordsucc n) ⊆ SNoS_ ω.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply L_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ v ⊆ SNoS_ ω) to the current goal.

We will prove L_ X n ∪ {w + eps_ (ordsucc n)|w ∈ L_ X n} ⊆ SNoS_ ω.

Apply binunion_Subq_min to the current goal.

An exact proof term for the current goal is IHn.

We will prove {w + eps_ (ordsucc n)|w ∈ L_ X n} ⊆ SNoS_ ω.

Let u be given.

Assume Hu.

Apply ReplE_impred (L_ X n) (λw ⇒ w + eps_ (ordsucc n)) u Hu to the current goal.

Let w be given.

Assume Hw: w ∈ L_ X n.

Assume Huw: u = w + eps_ (ordsucc n).

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

We will prove w + eps_ (ordsucc n) ∈ SNoS_ ω.

Apply add_SNo_SNoS_omega to the current goal.

An exact proof term for the current goal is IHn w Hw.

We will prove eps_ (ordsucc n) ∈ SNoS_ ω.

An exact proof term for the current goal is SNo_eps_SNoS_omega (ordsucc n) (omega_ordsucc n (nat_p_omega n Hn)).

Assume H1: n ∉ X.

Apply L_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ v ⊆ SNoS_ ω) to the current goal.

An exact proof term for the current goal is IHn.

We prove the intermediate claim R_SNo: ∀X, ∀n, nat_p n → R_ X n ⊆ SNoS_ ω.

Let X be given.

Apply nat_ind to the current goal.

We will prove R_ X 0 ⊆ SNoS_ ω.

Apply R_0 X (λ_ v ⇒ v ⊆ SNoS_ ω) to the current goal.

We will prove {1} ⊆ SNoS_ ω.

Let u be given.

Assume Hu.

rewrite the current goal using SingE 1 u Hu (from left to right).

We will prove 1 ∈ SNoS_ ω.

Apply SNoS_I ω omega_ordinal 1 1 (nat_p_omega 1 nat_1) to the current goal.

We will prove SNo_ 1 1.

An exact proof term for the current goal is ordinal_SNo_ 1 (nat_p_ordinal 1 nat_1).

Let n be given.

Assume Hn.

Assume IHn: R_ X n ⊆ SNoS_ ω.

We will prove R_ X (ordsucc n) ⊆ SNoS_ ω.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply R_ordsucc_pos X n (nat_p_omega n Hn) H1 (λ_ v ⇒ v ⊆ SNoS_ ω) to the current goal.

An exact proof term for the current goal is IHn.

Assume H1: n ∉ X.

Apply R_ordsucc_neg X n (nat_p_omega n Hn) H1 (λ_ v ⇒ v ⊆ SNoS_ ω) to the current goal.

We will prove R_ X n ∪ {w + - eps_ (ordsucc n)|w ∈ R_ X n} ⊆ SNoS_ ω.

Apply binunion_Subq_min to the current goal.

An exact proof term for the current goal is IHn.

We will prove {w + - eps_ (ordsucc n)|w ∈ R_ X n} ⊆ SNoS_ ω.

Let u be given.

Assume Hu.

Apply ReplE_impred (R_ X n) (λw ⇒ w + - eps_ (ordsucc n)) u Hu to the current goal.

Let w be given.

Assume Hw: w ∈ R_ X n.

Assume Huw: u = w + - eps_ (ordsucc n).

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

We will prove w + - eps_ (ordsucc n) ∈ SNoS_ ω.

Apply add_SNo_SNoS_omega to the current goal.

An exact proof term for the current goal is IHn w Hw.

We will prove - eps_ (ordsucc n) ∈ SNoS_ ω.

Apply minus_SNo_SNoS_omega to the current goal.

We will prove eps_ (ordsucc n) ∈ SNoS_ ω.

An exact proof term for the current goal is SNo_eps_SNoS_omega (ordsucc n) (omega_ordsucc n (nat_p_omega n Hn)).

Set L to be the term λX ⇒ ⋃_{n ∈ ω}L_ X n of type set → set.

Set R to be the term λX ⇒ ⋃_{n ∈ ω}R_ X n of type set → set.

We prove the intermediate claim LSo: ∀X, L X ⊆ SNoS_ ω.

Let X and u be given.

Assume Hu: u ∈ ⋃_{n ∈ ω}L_ X n.

Apply famunionE_impred ω (L_ X) u Hu to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hu: u ∈ L_ X n.

We will prove u ∈ SNoS_ ω.

An exact proof term for the current goal is L_SNo X n (omega_nat_p n Hn) u Hu.

We prove the intermediate claim RSo: ∀X, R X ⊆ SNoS_ ω.

Let X and u be given.

Assume Hu: u ∈ ⋃_{n ∈ ω}R_ X n.

Apply famunionE_impred ω (R_ X) u Hu to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hu: u ∈ R_ X n.

We will prove u ∈ SNoS_ ω.

An exact proof term for the current goal is R_SNo X n (omega_nat_p n Hn) u Hu.

We prove the intermediate claim LSNo: ∀X, ∀w ∈ L X, SNo w.

Let X and w be given.

Assume Hw.

Apply famunionE_impred ω (L_ X) w Hw to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hw': w ∈ L_ X n.

An exact proof term for the current goal is L_SNo1 X n (omega_nat_p n Hn) w Hw'.

We prove the intermediate claim RSNo: ∀X, ∀z ∈ R X, SNo z.

Let X and z be given.

Assume Hz.

Apply famunionE_impred ω (R_ X) z Hz to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hz': z ∈ R_ X n.

An exact proof term for the current goal is R_SNo1 X n (omega_nat_p n Hn) z Hz'.

We prove the intermediate claim LLR: ∀X, SNoCutP (L X) (R X).

Let X be given.

We will prove (∀w ∈ L X, SNo w) ∧ (∀z ∈ R X, SNo z) ∧ (∀w ∈ L X, ∀z ∈ R X, w < z).

Apply and3I to the current goal.

An exact proof term for the current goal is LSNo X.

An exact proof term for the current goal is RSNo X.

Let w be given.

Assume Hw.

Let z be given.

Assume Hz.

We prove the intermediate claim Lw: SNo w.

An exact proof term for the current goal is LSNo X w Hw.

We prove the intermediate claim Lz: SNo z.

An exact proof term for the current goal is RSNo X z Hz.

We prove the intermediate claim Lwzn: ∀n, nat_p n → w ∈ L_ X n → z ∈ R_ X n → w < z.

Let n be given.

Assume Hn.

Assume H1: w ∈ L_ X n.

Assume H2: z ∈ R_ X n.

We will prove w < z.

Apply finite_max_exists (L_ X n) (L_SNo1 X n Hn) (L_fin X n Hn) (L_ne X n Hn) to the current goal.

Let w' be given.

Assume Hw': SNo_max_of (L_ X n) w'.

Apply Hw' to the current goal.

Assume H.

Apply H to the current goal.

Assume Hw'1: w' ∈ L_ X n.

Assume Hw'2: SNo w'.

Assume Hw'3: ∀y ∈ L_ X n, SNo y → y ≤ w'.

Apply finite_min_exists (R_ X n) (R_SNo1 X n Hn) (R_fin X n Hn) (R_ne X n Hn) to the current goal.

Let z' be given.

Assume Hz': SNo_min_of (R_ X n) z'.

Apply Hz' to the current goal.

Assume H.

Apply H to the current goal.

Assume Hz'1: z' ∈ R_ X n.

Assume Hz'2: SNo z'.

Assume Hz'3: ∀y ∈ R_ X n, SNo y → z' ≤ y.

We will prove w < z.

Apply SNoLeLt_tra w w' z Lw Hw'2 Lz (Hw'3 w H1 Lw) to the current goal.

We will prove w' < z.

Apply SNoLtLe_tra w' z' z Hw'2 Hz'2 Lz to the current goal.

We will prove w' < z'.

rewrite the current goal using L_R_dist X n Hn w' z' Hw' Hz' (from left to right).

We will prove w' < w' + eps_ n.

An exact proof term for the current goal is add_SNo_eps_Lt w' Hw'2 n (nat_p_omega n Hn).

We will prove z' ≤ z.

An exact proof term for the current goal is Hz'3 z H2 Lz.

Apply famunionE_impred ω (L_ X) w Hw to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hw': w ∈ L_ X n.

Apply famunionE_impred ω (R_ X) z Hz to the current goal.

Let m be given.

Assume Hm: m ∈ ω.

Assume Hz': z ∈ R_ X m.

We will prove w < z.

Apply ordinal_trichotomy_or_impred m n (nat_p_ordinal m (omega_nat_p m Hm)) (nat_p_ordinal n (omega_nat_p n Hn)) to the current goal.

Assume H1: m ∈ n.

Apply Lwzn n (omega_nat_p n Hn) to the current goal.

We will prove w ∈ L_ X n.

An exact proof term for the current goal is Hw'.

We will prove z ∈ R_ X n.

An exact proof term for the current goal is R_Subq X n (omega_nat_p n Hn) m H1 z Hz'.

Assume H1: m = n.

Apply Lwzn n (omega_nat_p n Hn) to the current goal.

We will prove w ∈ L_ X n.

An exact proof term for the current goal is Hw'.

We will prove z ∈ R_ X n.

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

An exact proof term for the current goal is Hz'.

Assume H1: n ∈ m.

Apply Lwzn m (omega_nat_p m Hm) to the current goal.

We will prove w ∈ L_ X m.

An exact proof term for the current goal is L_Subq X m (omega_nat_p m Hm) n H1 w Hw'.

We will prove z ∈ R_ X m.

An exact proof term for the current goal is Hz'.

We prove the intermediate claim L0_In: ∀X, 0 ∈ L X.

Let X be given.

We will prove 0 ∈ ⋃_{n ∈ ω}L_ X n.

Apply famunionI ω (L_ X) 0 0 to the current goal.

We will prove 0 ∈ ω.

Apply nat_p_omega to the current goal.

We will prove nat_p 0.

An exact proof term for the current goal is nat_0.

We will prove 0 ∈ L_ X 0.

An exact proof term for the current goal is L_0_In X 0 nat_0.

We prove the intermediate claim R1_In: ∀X, 1 ∈ R X.

Let X be given.

We will prove 1 ∈ ⋃_{n ∈ ω}R_ X n.

Apply famunionI ω (R_ X) 0 1 to the current goal.

We will prove 0 ∈ ω.

Apply nat_p_omega to the current goal.

We will prove nat_p 0.

An exact proof term for the current goal is nat_0.

We will prove 1 ∈ R_ X 0.

An exact proof term for the current goal is R_1_In X 0 nat_0.

We prove the intermediate claim Lne: ∀X, L X ≠ 0.

Let X be given.

Assume H1: L X = 0.

Apply EmptyE 0 to the current goal.

We will prove 0 ∈ 0.

rewrite the current goal using H1 (from right to left) at position 2.

An exact proof term for the current goal is L0_In X.

We prove the intermediate claim Rne: ∀X, R X ≠ 0.

Let X be given.

Assume H1: R X = 0.

Apply EmptyE 1 to the current goal.

We will prove 1 ∈ 0.

rewrite the current goal using H1 (from right to left) at position 2.

An exact proof term for the current goal is R1_In X.

We prove the intermediate claim L_nomax: ∀X ⊆ ω, infinite X → ∀w ∈ L X, ∃w' ∈ L X, w < w'.

Let X be given.

Assume HX1 HX2.

Let w be given.

Assume Hw.

We prove the intermediate claim Lw: SNo w.

An exact proof term for the current goal is LSNo X w Hw.

Apply famunionE_impred ω (L_ X) w Hw to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hw': w ∈ L_ X n.

Apply infinite_bigger X HX1 HX2 n Hn to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume Hm: m ∈ X.

Assume Hnm: n ∈ m.

We prove the intermediate claim Lwm: w ∈ L_ X m.

An exact proof term for the current goal is L_Subq X m (omega_nat_p m (HX1 m Hm)) n Hnm w Hw'.

We prove the intermediate claim LweSm1: w + eps_ (ordsucc m) ∈ L_ X m ∪ {w + eps_ (ordsucc m)|w ∈ L_ X m}.

Apply binunionI2 to the current goal.

We will prove w + eps_ (ordsucc m) ∈ {w + eps_ (ordsucc m)|w ∈ L_ X m}.

An exact proof term for the current goal is ReplI (L_ X m) (λw ⇒ w + eps_ (ordsucc m)) w Lwm.

We prove the intermediate claim LweSm2: w + eps_ (ordsucc m) ∈ L_ X (ordsucc m).

An exact proof term for the current goal is L_ordsucc_pos X m (HX1 m Hm) Hm (λ_ v ⇒ w + eps_ (ordsucc m) ∈ v) LweSm1.

We use (w + eps_ (ordsucc m)) to witness the existential quantifier.

Apply andI to the current goal.

We will prove w + eps_ (ordsucc m) ∈ L X.

We will prove w + eps_ (ordsucc m) ∈ ⋃_{n ∈ ω}L_ X n.

An exact proof term for the current goal is famunionI ω (L_ X) (ordsucc m) (w + eps_ (ordsucc m)) (omega_ordsucc m (HX1 m Hm)) LweSm2.

We will prove w < w + eps_ (ordsucc m).

An exact proof term for the current goal is add_SNo_eps_Lt w Lw (ordsucc m) (omega_ordsucc m (HX1 m Hm)).

We prove the intermediate claim R_nomin: ∀X ⊆ ω, infinite (ω ∖ X) → ∀z ∈ R X, ∃z' ∈ R X, z' < z.

Let X be given.

Assume HX1 HX2.

Let z be given.

Assume Hz.

We prove the intermediate claim Lz: SNo z.

An exact proof term for the current goal is RSNo X z Hz.

Apply famunionE_impred ω (R_ X) z Hz to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hz': z ∈ R_ X n.

Apply infinite_bigger (ω ∖ X) (setminus_Subq ω X) HX2 n Hn to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume Hm: m ∈ ω ∖ X.

Assume Hnm: n ∈ m.

Apply setminusE ω X m Hm to the current goal.

Assume Hm1: m ∈ ω.

Assume Hm2: m ∉ X.

We prove the intermediate claim Lzm: z ∈ R_ X m.

An exact proof term for the current goal is R_Subq X m (omega_nat_p m Hm1) n Hnm z Hz'.

We prove the intermediate claim LzmeSm1: z + - eps_ (ordsucc m) ∈ R_ X m ∪ {z + - eps_ (ordsucc m)|z ∈ R_ X m}.

Apply binunionI2 to the current goal.

We will prove z + - eps_ (ordsucc m) ∈ {z + - eps_ (ordsucc m)|z ∈ R_ X m}.

An exact proof term for the current goal is ReplI (R_ X m) (λz ⇒ z + - eps_ (ordsucc m)) z Lzm.

We prove the intermediate claim LzmeSm2: z + - eps_ (ordsucc m) ∈ R_ X (ordsucc m).

An exact proof term for the current goal is R_ordsucc_neg X m Hm1 Hm2 (λ_ v ⇒ z + - eps_ (ordsucc m) ∈ v) LzmeSm1.

We use (z + - eps_ (ordsucc m)) to witness the existential quantifier.

Apply andI to the current goal.

We will prove z + - eps_ (ordsucc m) ∈ R X.

We will prove z + - eps_ (ordsucc m) ∈ ⋃_{n ∈ ω}R_ X n.

An exact proof term for the current goal is famunionI ω (R_ X) (ordsucc m) (z + - eps_ (ordsucc m)) (omega_ordsucc m Hm1) LzmeSm2.

We will prove z + - eps_ (ordsucc m) < z.

rewrite the current goal using add_SNo_0R z Lz (from right to left) at position 2.

We will prove z + - eps_ (ordsucc m) < z + 0.

Apply add_SNo_Lt2 z (- eps_ (ordsucc m)) 0 Lz (SNo_minus_SNo (eps_ (ordsucc m)) (SNo_eps_ (ordsucc m) (omega_ordsucc m Hm1))) SNo_0 to the current goal.

We will prove - eps_ (ordsucc m) < 0.

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

We will prove - eps_ (ordsucc m) < - 0.

An exact proof term for the current goal is minus_SNo_Lt_contra 0 (eps_ (ordsucc m)) SNo_0 (SNo_eps_ (ordsucc m) (omega_ordsucc m Hm1)) (SNo_eps_pos (ordsucc m) (omega_ordsucc m Hm1)).

We prove the intermediate claim L_R_real: ∀X ⊆ ω, infinite X → infinite (ω ∖ X) → SNoCut (L X) (R X) ∈ real.

Let X be given.

Assume HXo HXinf HXcoinf.

An exact proof term for the current goal is real_SNoCut_SNoS_omega (L X) (LSo X) (R X) (RSo X) (LLR X) (Lne X) (Rne X) (L_nomax X HXo HXinf) (R_nomin X HXo HXcoinf).

We prove the intermediate claim L_R_pos: ∀X, 0 < SNoCut (L X) (R X).

Let X be given.

Apply SNoCutP_SNoCut_impred (L X) (R X) (LLR X) to the current goal.

Assume HLR1: SNo (SNoCut (L X) (R X)).

Assume _.

Assume HLR3: ∀w ∈ L X, w < SNoCut (L X) (R X).

Assume HLR4: ∀z ∈ R X, SNoCut (L X) (R X) < z.

Assume _.

Apply HLR3 to the current goal.

An exact proof term for the current goal is L0_In X.

We prove the intermediate claim L_R_lt1: ∀X, SNoCut (L X) (R X) < 1.

Let X be given.

Apply SNoCutP_SNoCut_impred (L X) (R X) (LLR X) to the current goal.

Assume HLR1: SNo (SNoCut (L X) (R X)).

Assume _.

Assume HLR3: ∀w ∈ L X, w < SNoCut (L X) (R X).

Assume HLR4: ∀z ∈ R X, SNoCut (L X) (R X) < z.

Assume _.

Apply HLR4 to the current goal.

An exact proof term for the current goal is R1_In X.

We prove the intermediate claim L_R_inj: ∀X Y ⊆ ω, SNoCut (L X) (R X) = SNoCut (L Y) (R Y) → ∀n, nat_p n → L_ X n = L_ Y n ∧ R_ X n = R_ Y n ∧ (∀i ∈ n, i ∈ X ↔ i ∈ Y).

Let X be given.

Assume HX.

Let Y be given.

Assume HY.

Assume HXY: SNoCut (L X) (R X) = SNoCut (L Y) (R Y).

We will prove ∀n, nat_p n → L_ X n = L_ Y n ∧ R_ X n = R_ Y n ∧ (∀i ∈ n, i ∈ X ↔ i ∈ Y).

Apply SNoCutP_SNoCut_impred (L X) (R X) (LLR X) to the current goal.

Assume HLRX1: SNo (SNoCut (L X) (R X)).

Assume HLRX2.

Assume HLRX3: ∀w ∈ L X, w < SNoCut (L X) (R X).

Assume HLRX4: ∀z ∈ R X, SNoCut (L X) (R X) < z.

Assume HLRX5.

Apply SNoCutP_SNoCut_impred (L Y) (R Y) (LLR Y) to the current goal.

Assume HLRY1: SNo (SNoCut (L Y) (R Y)).

Assume HLRY2.

Assume HLRY3: ∀w ∈ L Y, w < SNoCut (L Y) (R Y).

Assume HLRY4: ∀z ∈ R Y, SNoCut (L Y) (R Y) < z.

Assume HLRY5.

Apply nat_ind to the current goal.

We will prove L_ X 0 = L_ Y 0 ∧ R_ X 0 = R_ Y 0 ∧ (∀i ∈ 0, i ∈ X ↔ i ∈ Y).

Apply and3I to the current goal.

We will prove L_ X 0 = L_ Y 0.

Use transitivity with and {0}.

An exact proof term for the current goal is L_0 X.

Use symmetry.

An exact proof term for the current goal is L_0 Y.

We will prove R_ X 0 = R_ Y 0.

Use transitivity with and {1}.

An exact proof term for the current goal is R_0 X.

Use symmetry.

An exact proof term for the current goal is R_0 Y.

Let i be given.

Assume Hi: i ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE i Hi.

Let n be given.

Assume Hn.

Assume IHn.

Apply IHn to the current goal.

Assume H.

Apply H to the current goal.

Assume IHLn: L_ X n = L_ Y n.

Assume IHRn: R_ X n = R_ Y n.

Assume IHnXY: ∀i ∈ n, i ∈ X ↔ i ∈ Y.

We will prove L_ X (ordsucc n) = L_ Y (ordsucc n) ∧ R_ X (ordsucc n) = R_ Y (ordsucc n) ∧ (∀i ∈ ordsucc n, i ∈ X ↔ i ∈ Y).

We prove the intermediate claim Ln: n ∈ ω.

An exact proof term for the current goal is nat_p_omega n Hn.

We prove the intermediate claim Len: SNo (eps_ n).

An exact proof term for the current goal is SNo_eps_ n Ln.

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

An exact proof term for the current goal is omega_ordsucc n Ln.

We prove the intermediate claim LeSn: SNo (eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_eps_ (ordsucc n) LSn.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply xm (n ∈ Y) to the current goal.

Assume H2: n ∈ Y.

Apply and3I to the current goal.

We will prove L_ X (ordsucc n) = L_ Y (ordsucc n).

Use transitivity with L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n}, and L_ Y n ∪ {x + eps_ (ordsucc n)|x ∈ L_ Y n}.

An exact proof term for the current goal is L_ordsucc_pos X n Ln H1.

We will prove L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n} = L_ Y n ∪ {x + eps_ (ordsucc n)|x ∈ L_ Y n}.

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

Use reflexivity.

Use symmetry.

An exact proof term for the current goal is L_ordsucc_pos Y n Ln H2.

We will prove R_ X (ordsucc n) = R_ Y (ordsucc n).

Use transitivity with R_ X n, and R_ Y n.

An exact proof term for the current goal is R_ordsucc_pos X n Ln H1.

We will prove R_ X n = R_ Y n.

An exact proof term for the current goal is IHRn.

Use symmetry.

An exact proof term for the current goal is R_ordsucc_pos Y n Ln H2.

Let i be given.

Assume Hi: i ∈ ordsucc n.

Apply ordsuccE n i Hi to the current goal.

Assume Hi': i ∈ n.

An exact proof term for the current goal is IHnXY i Hi'.

Assume Hi': i = n.

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

We will prove n ∈ X ↔ n ∈ Y.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is H2.

Assume _.

An exact proof term for the current goal is H1.

Assume H2: n ∉ Y.

We will prove False.

Apply finite_max_exists (L_ X n) (L_SNo1 X n Hn) (L_fin X n Hn) (L_ne X n Hn) to the current goal.

Let w be given.

Assume Hw: SNo_max_of (L_ X n) w.

Apply Hw to the current goal.

Assume H.

Apply H to the current goal.

Assume Hw1: w ∈ L_ X n.

Assume Hw2: SNo w.

Assume Hw3: ∀y ∈ L_ X n, SNo y → y ≤ w.

Apply finite_min_exists (R_ X n) (R_SNo1 X n Hn) (R_fin X n Hn) (R_ne X n Hn) to the current goal.

Let z be given.

Assume Hz: SNo_min_of (R_ X n) z.

Apply Hz to the current goal.

Assume H.

Apply H to the current goal.

Assume Hz1: z ∈ R_ X n.

Assume Hz2: SNo z.

Assume Hz3: ∀y ∈ R_ X n, SNo y → z ≤ y.

We prove the intermediate claim LweSn: SNo (w + eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo w (eps_ (ordsucc n)) Hw2 LeSn.

Apply SNoLt_irref (w + eps_ (ordsucc n)) to the current goal.

We will prove w + eps_ (ordsucc n) < w + eps_ (ordsucc n).

Apply SNoLt_tra (w + eps_ (ordsucc n)) (SNoCut (L X) (R X)) (w + eps_ (ordsucc n)) ?? ?? ?? to the current goal.

We will prove w + eps_ (ordsucc n) < SNoCut (L X) (R X).

Apply HLRX3 to the current goal.

We will prove w + eps_ (ordsucc n) ∈ L X.

We will prove w + eps_ (ordsucc n) ∈ ⋃_{n ∈ ω}L_ X n.

Apply famunionI ω (L_ X) (ordsucc n) (w + eps_ (ordsucc n)) LSn to the current goal.

We will prove w + eps_ (ordsucc n) ∈ L_ X (ordsucc n).

We prove the intermediate claim LwLSn: w + eps_ (ordsucc n) ∈ L_ X n ∪ {x + eps_ (ordsucc n)|x ∈ L_ X n}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI (L_ X n) (λx ⇒ x + eps_ (ordsucc n)) w Hw1.

An exact proof term for the current goal is L_ordsucc_pos X n Ln H1 (λ_ u ⇒ w + eps_ (ordsucc n) ∈ u) LwLSn.

We will prove SNoCut (L X) (R X) < w + eps_ (ordsucc n).

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

We will prove SNoCut (L Y) (R Y) < w + eps_ (ordsucc n).

Apply HLRY4 to the current goal.

We will prove w + eps_ (ordsucc n) ∈ R Y.

We will prove w + eps_ (ordsucc n) ∈ ⋃_{n ∈ ω}R_ Y n.

Apply famunionI ω (R_ Y) (ordsucc n) (w + eps_ (ordsucc n)) LSn to the current goal.

We will prove w + eps_ (ordsucc n) ∈ R_ Y (ordsucc n).

We prove the intermediate claim Lwz: w + eps_ (ordsucc n) = z + - eps_ (ordsucc n).

rewrite the current goal using L_R_dist X n Hn w z Hw Hz (from left to right).

We will prove w + eps_ (ordsucc n) = (w + eps_ n) + - eps_ (ordsucc n).

rewrite the current goal using eps_ordsucc_half_add n Hn (from right to left).

We will prove w + eps_ (ordsucc n) = (w + eps_ (ordsucc n) + eps_ (ordsucc n)) + - eps_ (ordsucc n).

rewrite the current goal using add_SNo_assoc w (eps_ (ordsucc n)) (eps_ (ordsucc n)) Hw2 LeSn LeSn (from left to right).

We will prove w + eps_ (ordsucc n) = ((w + eps_ (ordsucc n)) + eps_ (ordsucc n)) + - eps_ (ordsucc n).

Use symmetry.

An exact proof term for the current goal is add_SNo_minus_R2 (w + eps_ (ordsucc n)) (eps_ (ordsucc n)) LweSn LeSn.

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

We will prove z + - eps_ (ordsucc n) ∈ R_ Y (ordsucc n).

We prove the intermediate claim Lz1: z ∈ R_ Y n.

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

An exact proof term for the current goal is Hz1.

We prove the intermediate claim LzRSn: z + - eps_ (ordsucc n) ∈ R_ Y n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ Y n}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI (R_ Y n) (λx ⇒ x + - eps_ (ordsucc n)) z Lz1.

An exact proof term for the current goal is R_ordsucc_neg Y n Ln H2 (λ_ u ⇒ z + - eps_ (ordsucc n) ∈ u) LzRSn.

Assume H1: n ∉ X.

Apply xm (n ∈ Y) to the current goal.

Assume H2: n ∈ Y.

We will prove False.

Apply finite_max_exists (L_ X n) (L_SNo1 X n Hn) (L_fin X n Hn) (L_ne X n Hn) to the current goal.

Let w be given.

Assume Hw: SNo_max_of (L_ X n) w.

Apply Hw to the current goal.

Assume H.

Apply H to the current goal.

Assume Hw1: w ∈ L_ X n.

Assume Hw2: SNo w.

Assume Hw3: ∀y ∈ L_ X n, SNo y → y ≤ w.

Apply finite_min_exists (R_ X n) (R_SNo1 X n Hn) (R_fin X n Hn) (R_ne X n Hn) to the current goal.

Let z be given.

Assume Hz: SNo_min_of (R_ X n) z.

Apply Hz to the current goal.

Assume H.

Apply H to the current goal.

Assume Hz1: z ∈ R_ X n.

Assume Hz2: SNo z.

Assume Hz3: ∀y ∈ R_ X n, SNo y → z ≤ y.

We prove the intermediate claim LweSn: SNo (w + eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_add_SNo w (eps_ (ordsucc n)) Hw2 LeSn.

Apply SNoLt_irref (w + eps_ (ordsucc n)) to the current goal.

We will prove w + eps_ (ordsucc n) < w + eps_ (ordsucc n).

Apply SNoLt_tra (w + eps_ (ordsucc n)) (SNoCut (L X) (R X)) (w + eps_ (ordsucc n)) ?? ?? ?? to the current goal.

We will prove w + eps_ (ordsucc n) < SNoCut (L X) (R X).

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

We will prove w + eps_ (ordsucc n) < SNoCut (L Y) (R Y).

Apply HLRY3 to the current goal.

We will prove w + eps_ (ordsucc n) ∈ L Y.

We will prove w + eps_ (ordsucc n) ∈ ⋃_{n ∈ ω}L_ Y n.

Apply famunionI ω (L_ Y) (ordsucc n) (w + eps_ (ordsucc n)) LSn to the current goal.

We will prove w + eps_ (ordsucc n) ∈ L_ Y (ordsucc n).

We prove the intermediate claim Lw1: w ∈ L_ Y n.

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

An exact proof term for the current goal is Hw1.

We prove the intermediate claim LwLSn: w + eps_ (ordsucc n) ∈ L_ Y n ∪ {x + eps_ (ordsucc n)|x ∈ L_ Y n}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI (L_ Y n) (λx ⇒ x + eps_ (ordsucc n)) w Lw1.

An exact proof term for the current goal is L_ordsucc_pos Y n Ln H2 (λ_ u ⇒ w + eps_ (ordsucc n) ∈ u) LwLSn.

We will prove SNoCut (L X) (R X) < w + eps_ (ordsucc n).

Apply HLRX4 to the current goal.

We will prove w + eps_ (ordsucc n) ∈ R X.

We will prove w + eps_ (ordsucc n) ∈ ⋃_{n ∈ ω}R_ X n.

Apply famunionI ω (R_ X) (ordsucc n) (w + eps_ (ordsucc n)) LSn to the current goal.

We will prove w + eps_ (ordsucc n) ∈ R_ X (ordsucc n).

We prove the intermediate claim Lwz: w + eps_ (ordsucc n) = z + - eps_ (ordsucc n).

rewrite the current goal using L_R_dist X n Hn w z Hw Hz (from left to right).

We will prove w + eps_ (ordsucc n) = (w + eps_ n) + - eps_ (ordsucc n).

rewrite the current goal using eps_ordsucc_half_add n Hn (from right to left).

We will prove w + eps_ (ordsucc n) = (w + eps_ (ordsucc n) + eps_ (ordsucc n)) + - eps_ (ordsucc n).

rewrite the current goal using add_SNo_assoc w (eps_ (ordsucc n)) (eps_ (ordsucc n)) Hw2 LeSn LeSn (from left to right).

We will prove w + eps_ (ordsucc n) = ((w + eps_ (ordsucc n)) + eps_ (ordsucc n)) + - eps_ (ordsucc n).

Use symmetry.

An exact proof term for the current goal is add_SNo_minus_R2 (w + eps_ (ordsucc n)) (eps_ (ordsucc n)) LweSn LeSn.

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

We will prove z + - eps_ (ordsucc n) ∈ R_ X (ordsucc n).

We prove the intermediate claim LzRSn: z + - eps_ (ordsucc n) ∈ R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI (R_ X n) (λx ⇒ x + - eps_ (ordsucc n)) z Hz1.

An exact proof term for the current goal is R_ordsucc_neg X n Ln H1 (λ_ u ⇒ z + - eps_ (ordsucc n) ∈ u) LzRSn.

Assume H2: n ∉ Y.

Apply and3I to the current goal.

We will prove L_ X (ordsucc n) = L_ Y (ordsucc n).

Use transitivity with L_ X n, and L_ Y n.

An exact proof term for the current goal is L_ordsucc_neg X n Ln H1.

We will prove L_ X n = L_ Y n.

An exact proof term for the current goal is IHLn.

Use symmetry.

An exact proof term for the current goal is L_ordsucc_neg Y n Ln H2.

We will prove R_ X (ordsucc n) = R_ Y (ordsucc n).

Use transitivity with R_ X n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ X n}, and R_ Y n ∪ {x + - eps_ (ordsucc n)|x ∈ R_ Y n}.

An exact proof term for the current goal is R_ordsucc_neg X n Ln H1.

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

Use reflexivity.

Use symmetry.

An exact proof term for the current goal is R_ordsucc_neg Y n Ln H2.

Let i be given.

Assume Hi: i ∈ ordsucc n.

Apply ordsuccE n i Hi to the current goal.

Assume Hi': i ∈ n.

An exact proof term for the current goal is IHnXY i Hi'.

Assume Hi': i = n.

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

We will prove n ∈ X ↔ n ∈ Y.

Apply iffI to the current goal.

Assume H3.

We will prove False.

An exact proof term for the current goal is H1 H3.

Assume H4.

We will prove False.

An exact proof term for the current goal is H2 H4.

Set s to be the term λX ⇒ {0} ∪ {ordsucc n|n ∈ X} of type set → set.

We prove the intermediate claim Ls: ∀X ∈ 𝒫 ω, s X ∈ 𝒫 ω.

Let X be given.

Assume HX.

Apply PowerI to the current goal.

We will prove {0} ∪ {ordsucc n|n ∈ X} ⊆ ω.

Apply binunion_Subq_min to the current goal.

We will prove {0} ⊆ ω.

Let u be given.

Assume Hu: u ∈ {0}.

rewrite the current goal using SingE 0 u Hu (from left to right).

We will prove 0 ∈ ω.

An exact proof term for the current goal is nat_p_omega 0 nat_0.

We will prove {ordsucc n|n ∈ X} ⊆ ω.

Let u be given.

Assume Hu.

Apply ReplE_impred X ordsucc u Hu to the current goal.

Let n be given.

Assume Hn: n ∈ X.

Assume Hun: u = ordsucc n.

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

Apply omega_ordsucc n to the current goal.

We will prove n ∈ ω.

An exact proof term for the current goal is PowerE ω X HX n Hn.

We prove the intermediate claim Lsinj: ∀X Y, s X = s Y → X = Y.

Let X and Y be given.

Assume HXY: s X = s Y.

Apply set_ext to the current goal.

Let u be given.

Assume Hu: u ∈ X.

We prove the intermediate claim LSu: ordsucc u ∈ s Y.

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

We will prove ordsucc u ∈ {0} ∪ {ordsucc n|n ∈ X}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI X ordsucc u Hu.

Apply binunionE {0} {ordsucc n|n ∈ Y} (ordsucc u) LSu to the current goal.

Assume H1: ordsucc u ∈ {0}.

We will prove False.

Apply neq_ordsucc_0 u to the current goal.

An exact proof term for the current goal is SingE 0 (ordsucc u) H1.

Assume H1: ordsucc u ∈ {ordsucc n|n ∈ Y}.

Apply ReplE_impred Y ordsucc (ordsucc u) H1 to the current goal.

Let n be given.

Assume Hn: n ∈ Y.

Assume HSun: ordsucc u = ordsucc n.

We will prove u ∈ Y.

rewrite the current goal using ordsucc_inj u n HSun (from left to right).

An exact proof term for the current goal is Hn.

Let u be given.

Assume Hu: u ∈ Y.

We prove the intermediate claim LSu: ordsucc u ∈ s X.

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

We will prove ordsucc u ∈ {0} ∪ {ordsucc n|n ∈ Y}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI Y ordsucc u Hu.

Apply binunionE {0} {ordsucc n|n ∈ X} (ordsucc u) LSu to the current goal.

Assume H1: ordsucc u ∈ {0}.

We will prove False.

Apply neq_ordsucc_0 u to the current goal.

An exact proof term for the current goal is SingE 0 (ordsucc u) H1.

Assume H1: ordsucc u ∈ {ordsucc n|n ∈ X}.

Apply ReplE_impred X ordsucc (ordsucc u) H1 to the current goal.

Let n be given.

Assume Hn: n ∈ X.

Assume HSun: ordsucc u = ordsucc n.

We will prove u ∈ X.

rewrite the current goal using ordsucc_inj u n HSun (from left to right).

An exact proof term for the current goal is Hn.

We prove the intermediate claim Ls0: ∀X, 0 ∈ s X.

Let X be given.

An exact proof term for the current goal is binunionI1 {0} {ordsucc n|n ∈ X} 0 (SingI 0).

We prove the intermediate claim Lsfin: ∀X, finite X → finite (s X).

Let X be given.

Assume HX.

We will prove finite ({0} ∪ {ordsucc n|n ∈ X}).

Apply binunion_finite to the current goal.

Apply Sing_finite to the current goal.

Apply Repl_finite to the current goal.

An exact proof term for the current goal is HX.

Set h to be the term λX ⇒ X ∪ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X} of type set → set.

We prove the intermediate claim Lh0: h 0 = 0.

We will prove 0 ∪ (⋃_{i ∈ 0}{n '|n ∈ i, n ∉ 0}) = 0.

rewrite the current goal using famunion_Empty (λi ⇒ {n '|n ∈ i, n ∉ 0}) (from left to right).

We will prove 0 ∪ 0 = 0.

An exact proof term for the current goal is binunion_idl 0.

We prove the intermediate claim LhSa: ∀X ∈ 𝒫 ω, ∀α, ordinal α → X ⊆ α → (∀n ∈ α, ¬ (X ⊆ n)) → SNo_ α (h X).

Let X be given.

Assume HX: X ∈ 𝒫 ω.

Let α be given.

Assume Ha1: ordinal α.

Assume Ha2: X ⊆ α.

Assume Ha3: ∀n ∈ α, ¬ (X ⊆ n).

Apply Ha1 to the current goal.

Assume Ha1a Ha1b.

We will prove SNo_ α (h X).

We will prove h X ⊆ SNoElts_ α ∧ ∀n ∈ α, exactly1of2 (n ' ∈ h X) (n ∈ h X).

Apply andI to the current goal.

Let u be given.

Assume Hu: u ∈ h X.

We will prove u ∈ SNoElts_ α.

Apply binunionE X (⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}) u Hu to the current goal.

Assume H1: u ∈ X.

We will prove u ∈ α ∪ {n '|n ∈ α}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Ha2 u H1.

Assume H1: u ∈ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

We will prove u ∈ α ∪ {n '|n ∈ α}.

Apply binunionI2 to the current goal.

We will prove u ∈ {n '|n ∈ α}.

Apply famunionE_impred X (λi ⇒ {n '|n ∈ i, n ∉ X}) u H1 to the current goal.

Let i be given.

Assume Hi: i ∈ X.

Assume H2: u ∈ {n '|n ∈ i, n ∉ X}.

Apply ReplSepE_impred i (λn ⇒ n ∉ X) (λn ⇒ n ') u H2 to the current goal.

Let n be given.

Assume Hn: n ∈ i.

Assume H3: n ∉ X.

Assume H4: u = n '.

We will prove u ∈ {n '|n ∈ α}.

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

We prove the intermediate claim Lna: n ∈ α.

An exact proof term for the current goal is Ha1a i (Ha2 i Hi) n Hn.

An exact proof term for the current goal is ReplI α (λn ⇒ n ') n Lna.

Let n be given.

Assume Hn: n ∈ α.

We will prove exactly1of2 (n ' ∈ h X) (n ∈ h X).

We prove the intermediate claim Lno: ordinal n.

An exact proof term for the current goal is ordinal_Hered α Ha1 n Hn.

Apply xm (n ∈ X) to the current goal.

Assume H1: n ∈ X.

Apply exactly1of2_I2 to the current goal.

We will prove n ' ∉ h X.

Assume H2: n ' ∈ X ∪ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply binunionE X (⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}) (n ') H2 to the current goal.

Assume H3: n ' ∈ X.

Apply tagged_not_ordinal n to the current goal.

We will prove ordinal (n ').

Apply ordinal_Hered α Ha1 (n ') to the current goal.

We will prove n ' ∈ α.

An exact proof term for the current goal is Ha2 (n ') H3.

Assume H3: n ' ∈ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply famunionE_impred X (λi ⇒ {n '|n ∈ i, n ∉ X}) (n ') H3 to the current goal.

Let i be given.

Assume Hi: i ∈ X.

Assume H4: n ' ∈ {n '|n ∈ i, n ∉ X}.

Apply ReplSepE_impred i (λn ⇒ n ∉ X) (λn ⇒ n ') (n ') H4 to the current goal.

Let m be given.

Assume Hm: m ∈ i.

Assume H5: m ∉ X.

Assume H6: n ' = m '.

Apply H5 to the current goal.

We prove the intermediate claim Lmo: ordinal m.

Apply ordinal_Hered α Ha1 m to the current goal.

We will prove m ∈ α.

An exact proof term for the current goal is Ha1a i (Ha2 i Hi) m Hm.

rewrite the current goal using tagged_eqE_eq n m Lno Lmo H6 (from right to left).

An exact proof term for the current goal is H1.

We will prove n ∈ h X.

We will prove n ∈ X ∪ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H1.

Assume H1: n ∉ X.

Apply exactly1of2_I1 to the current goal.

We will prove n ' ∈ h X.

We will prove n ' ∈ X ∪ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply binunionI2 to the current goal.

We will prove n ' ∈ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply xm (∃i ∈ X, n ∈ i) to the current goal.

Assume H3: ∃i ∈ X, n ∈ i.

Apply H3 to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ X.

Assume Hni: n ∈ i.

We prove the intermediate claim Ln': n ' ∈ {n '|n ∈ i, n ∉ X}.

An exact proof term for the current goal is ReplSepI i (λn ⇒ n ∉ X) (λn ⇒ n ') n Hni H1.

An exact proof term for the current goal is famunionI X (λi ⇒ {n '|n ∈ i, n ∉ X}) i (n ') Hi Ln'.

Assume H3: ¬ ∃i ∈ X, n ∈ i.

We will prove False.

Apply Ha3 n Hn to the current goal.

We will prove X ⊆ n.

Let i be given.

Assume Hi: i ∈ X.

We will prove i ∈ n.

We prove the intermediate claim Lio: ordinal i.

An exact proof term for the current goal is ordinal_Hered α Ha1 i (Ha2 i Hi).

Apply ordinal_trichotomy_or_impred i n Lio Lno to the current goal.

Assume H4: i ∈ n.

An exact proof term for the current goal is H4.

Assume H4: i = n.

We will prove False.

Apply H1 to the current goal.

We will prove n ∈ X.

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

An exact proof term for the current goal is Hi.

Assume H4: n ∈ i.

We will prove False.

Apply H3 to the current goal.

We use i to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hi.

An exact proof term for the current goal is H4.

We will prove n ∉ h X.

Assume H2: n ∈ X ∪ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply binunionE X (⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}) n H2 to the current goal.

Assume H3: n ∈ X.

We will prove False.

An exact proof term for the current goal is H1 H3.

Assume H3: n ∈ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply famunionE_impred X (λi ⇒ {n '|n ∈ i, n ∉ X}) n H3 to the current goal.

Let i be given.

Assume Hi: i ∈ X.

Assume H4: n ∈ {n '|n ∈ i, n ∉ X}.

Apply ReplSepE_impred i (λn ⇒ n ∉ X) (λn ⇒ n ') n H4 to the current goal.

Let m be given.

Assume Hm: m ∈ i.

Assume H5: m ∉ X.

Assume H6: n = m '.

We will prove False.

Apply tagged_not_ordinal m to the current goal.

We will prove ordinal (m ').

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

An exact proof term for the current goal is Lno.

We prove the intermediate claim LhS: ∀X ∈ 𝒫 ω, SNo (h X).

Let X be given.

Assume HX: X ∈ 𝒫 ω.

We prove the intermediate claim LhS': ∃α, ordinal α ∧ X ⊆ α.

We use ω to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is omega_ordinal.

We will prove X ⊆ ω.

Apply PowerE to the current goal.

An exact proof term for the current goal is HX.

Apply least_ordinal_ex (λα ⇒ X ⊆ α) LhS' to the current goal.

Let α be given.

Assume H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume Ha1: ordinal α.

Assume Ha2: X ⊆ α.

Assume Ha3: ∀n ∈ α, ¬ (X ⊆ n).

Apply SNo_SNo α Ha1 (h X) to the current goal.

We will prove SNo_ α (h X).

An exact proof term for the current goal is LhSa X HX α Ha1 Ha2 Ha3.

We prove the intermediate claim Lh: ∀X ∈ 𝒫 ω, finite X → h X ∈ SNoS_ ω.

Let X be given.

Assume HX: X ∈ 𝒫 ω.

Assume HXfin: finite X.

We will prove h X ∈ SNoS_ ω.

Apply xm (X = 0) to the current goal.

Assume H1: X = 0.

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

We will prove h 0 ∈ SNoS_ ω.

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

We will prove 0 ∈ SNoS_ ω.

Apply SNoS_I ω omega_ordinal 0 0 (nat_p_omega 0 nat_0) to the current goal.

We will prove SNo_ 0 0.

An exact proof term for the current goal is ordinal_SNo_ Empty ordinal_Empty.

Assume H1: X ≠ 0.

We prove the intermediate claim LXS: ∀x ∈ X, SNo x.

Let x be given.

Assume Hx.

Apply nat_p_SNo to the current goal.

Apply omega_nat_p to the current goal.

We will prove x ∈ ω.

An exact proof term for the current goal is PowerE ω X HX x Hx.

Apply finite_max_exists X LXS HXfin H1 to the current goal.

Let n be given.

Assume Hn: SNo_max_of X n.

Apply Hn to the current goal.

Assume H.

Apply H to the current goal.

Assume Hn1: n ∈ X.

Assume Hn2: SNo n.

Assume Hn3: ∀x ∈ X, SNo x → x ≤ n.

We prove the intermediate claim Ln: n ∈ ω.

An exact proof term for the current goal is PowerE ω X HX n Hn1.

We prove the intermediate claim Lno: ordinal n.

Apply nat_p_ordinal to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Ln.

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

Apply omega_ordsucc to the current goal.

An exact proof term for the current goal is Ln.

We prove the intermediate claim LSno: ordinal (ordsucc n).

Apply nat_p_ordinal to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is LSn.

We prove the intermediate claim LSnhX: SNo_ (ordsucc n) (h X).

Apply LhSa X HX (ordsucc n) LSno to the current goal.

We will prove X ⊆ ordsucc n.

Let i be given.

Assume Hi: i ∈ X.

We prove the intermediate claim Lio: ordinal i.

An exact proof term for the current goal is ordinal_Hered ω omega_ordinal i (PowerE ω X HX i Hi).

We prove the intermediate claim LiS: SNo i.

An exact proof term for the current goal is ordinal_SNo i Lio.

Apply ordinal_In_Or_Subq i (ordsucc n) Lio LSno to the current goal.

Assume H2: i ∈ ordsucc n.

An exact proof term for the current goal is H2.

Assume H2: ordsucc n ⊆ i.

We will prove False.

Apply SNoLt_irref i to the current goal.

We will prove i < i.

Apply SNoLeLt_tra i n i LiS Hn2 LiS (Hn3 i Hi LiS) to the current goal.

We will prove n < i.

Apply SNoLtLe_tra n (ordsucc n) i (ordinal_SNo n Lno) (ordinal_SNo (ordsucc n) LSno) LiS to the current goal.

We will prove n < ordsucc n.

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

We will prove ordsucc n ≤ i.

An exact proof term for the current goal is ordinal_Subq_SNoLe (ordsucc n) i LSno Lio H2.

We will prove ∀m ∈ ordsucc n, ¬ (X ⊆ m).

Let m be given.

Assume Hm.

Assume H2: X ⊆ m.

Apply ordsuccE n m Hm to the current goal.

Assume H3: m ∈ n.

An exact proof term for the current goal is In_no2cycle m n H3 (H2 n Hn1).

Assume H3: m = n.

Apply In_irref n to the current goal.

rewrite the current goal using H3 (from right to left) at position 2.

We will prove n ∈ m.

An exact proof term for the current goal is H2 n Hn1.

We will prove h X ∈ SNoS_ ω.

An exact proof term for the current goal is SNoS_I ω omega_ordinal (h X) (ordsucc n) LSn LSnhX.

We prove the intermediate claim Lh0pos: ∀X ∈ 𝒫 ω, 0 ∈ X → 0 < h X.

Let X be given.

Assume HX HX0.

We will prove 0 < h X.

We prove the intermediate claim L0hX: 0 ∈ h X.

We will prove 0 ∈ X ∪ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is HX0.

Apply SNoLtI2 0 (h X) to the current goal.

We will prove SNoLev 0 ∈ SNoLev (h X).

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

We will prove 0 ∈ SNoLev (h X).

Apply SNoLev_ (h X) (LhS X HX) to the current goal.

Assume H1: h X ⊆ SNoElts_ (SNoLev (h X)).

Assume _.

Apply binunionE (SNoLev (h X)) {β '|β ∈ SNoLev (h X)} 0 (H1 0 L0hX) to the current goal.

Assume H2: 0 ∈ SNoLev (h X).

An exact proof term for the current goal is H2.

Assume H2: 0 ∈ {β '|β ∈ SNoLev (h X)}.

We will prove False.

Apply ReplE_impred (SNoLev (h X)) (λβ ⇒ β ') 0 H2 to the current goal.

Let β be given.

Assume Hb1: β ∈ SNoLev (h X).

Assume Hb2: 0 = β '.

Apply tagged_not_ordinal β to the current goal.

We will prove ordinal (β ').

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

An exact proof term for the current goal is ordinal_Empty.

We will prove SNoEq_ (SNoLev 0) 0 (h X).

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

Let i be given.

Assume Hi: i ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE i Hi.

We will prove SNoLev 0 ∈ h X.

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

An exact proof term for the current goal is L0hX.

We prove the intermediate claim Lhinj1: ∀X Y ∈ 𝒫 ω, h X = h Y → X ⊆ Y.

Let X be given.

Assume HX.

Let Y be given.

Assume HY HXY.

Let x be given.

Assume Hx: x ∈ X.

We prove the intermediate claim Lxo: ordinal x.

An exact proof term for the current goal is nat_p_ordinal x (omega_nat_p x (PowerE ω X HX x Hx)).

We prove the intermediate claim LxhY: x ∈ h Y.

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

We will prove x ∈ X ∪ ⋃_{i ∈ X}{n '|n ∈ i, n ∉ X}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hx.

Apply binunionE Y (⋃_{i ∈ Y}{n '|n ∈ i, n ∉ Y}) x LxhY to the current goal.

Assume H1: x ∈ Y.

An exact proof term for the current goal is H1.

Assume H1: x ∈ ⋃_{i ∈ Y}{n '|n ∈ i, n ∉ Y}.

Apply famunionE_impred Y (λi ⇒ {n '|n ∈ i, n ∉ Y}) x H1 to the current goal.

Let i be given.

Assume Hi: i ∈ Y.

Assume H2: x ∈ {n '|n ∈ i, n ∉ Y}.

Apply ReplSepE_impred i (λn ⇒ n ∉ Y) (λn ⇒ n ') x H2 to the current goal.

Let m be given.

Assume Hm: m ∈ i.

Assume H3: m ∉ Y.

Assume H4: x = m '.

We will prove False.

Apply tagged_not_ordinal m to the current goal.

We will prove ordinal (m ').

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

An exact proof term for the current goal is Lxo.

We prove the intermediate claim Lhinj: ∀X Y ∈ 𝒫 ω, h X = h Y → X = Y.

Let X be given.

Assume HX.

Let Y be given.

Assume HY HXY.

Apply set_ext to the current goal.

An exact proof term for the current goal is Lhinj1 X HX Y HY HXY.

An exact proof term for the current goal is Lhinj1 Y HY X HX (λq ⇒ HXY (λx y ⇒ q y x)).

Set g to be the term λX ⇒ if finite X then h (s X) + 1 else if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X) of type set → set.

We will prove ∃g : set → set, inj (𝒫 ω) real g.

We use g to witness the existential quantifier.

We will prove (∀u ∈ 𝒫 ω, g u ∈ real) ∧ (∀u v ∈ 𝒫 ω, g u = g v → u = v).

Apply andI to the current goal.

Let X be given.

Assume HX: X ∈ 𝒫 ω.

Apply xm (finite X) to the current goal.

Assume H1: finite X.

We will prove (if finite X then h (s X) + 1 else if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) ∈ real.

We prove the intermediate claim LhsX: h (s X) + 1 ∈ real.

Apply real_add_SNo to the current goal.

Apply SNoS_omega_real to the current goal.

Apply Lh to the current goal.

We will prove s X ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is HX.

We will prove finite (s X).

Apply Lsfin to the current goal.

An exact proof term for the current goal is H1.

We will prove 1 ∈ real.

Apply SNoS_omega_real to the current goal.

Apply omega_SNoS_omega to the current goal.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_1.

An exact proof term for the current goal is If_i_1 (finite X) (h (s X) + 1) (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) H1 (λ_ u ⇒ u ∈ real) LhsX.

Assume H1: infinite X.

Apply xm (finite (ω ∖ X)) to the current goal.

Assume H2: finite (ω ∖ X).

We prove the intermediate claim LmhsX: - h (s (ω ∖ X)) ∈ real.

Apply real_minus_SNo to the current goal.

Apply SNoS_omega_real to the current goal.

Apply Lh to the current goal.

We will prove s (ω ∖ X) ∈ 𝒫 ω.

Apply Ls to the current goal.

Apply PowerI to the current goal.

An exact proof term for the current goal is setminus_Subq ω X.

We will prove finite (s (ω ∖ X)).

Apply Lsfin to the current goal.

An exact proof term for the current goal is H2.

We prove the intermediate claim LmhsX': (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) ∈ real.

An exact proof term for the current goal is If_i_1 (finite (ω ∖ X)) (- h (s (ω ∖ X))) (SNoCut (L X) (R X)) H2 (λ_ u ⇒ u ∈ real) LmhsX.

An exact proof term for the current goal is If_i_0 (finite X) (h (s X) + 1) (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) H1 (λ_ u ⇒ u ∈ real) LmhsX'.

Assume H2: infinite (ω ∖ X).

We prove the intermediate claim LLRX: SNoCut (L X) (R X) ∈ real.

An exact proof term for the current goal is L_R_real X (PowerE ω X HX) H1 H2.

We prove the intermediate claim LLRX': (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) ∈ real.

An exact proof term for the current goal is If_i_0 (finite (ω ∖ X)) (- h (s (ω ∖ X))) (SNoCut (L X) (R X)) H2 (λ_ u ⇒ u ∈ real) LLRX.

An exact proof term for the current goal is If_i_0 (finite X) (h (s X) + 1) (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) H1 (λ_ u ⇒ u ∈ real) LLRX'.

Let X be given.

Assume HX: X ∈ 𝒫 ω.

Let Y be given.

Assume HY: Y ∈ 𝒫 ω.

We prove the intermediate claim LX: X ⊆ ω.

An exact proof term for the current goal is PowerE ω X HX.

We prove the intermediate claim LY: Y ⊆ ω.

An exact proof term for the current goal is PowerE ω Y HY.

We prove the intermediate claim LoX: ω ∖ X ∈ 𝒫 ω.

Apply PowerI to the current goal.

An exact proof term for the current goal is setminus_Subq ω X.

We prove the intermediate claim LoY: ω ∖ Y ∈ 𝒫 ω.

Apply PowerI to the current goal.

An exact proof term for the current goal is setminus_Subq ω Y.

Apply xm (finite X) to the current goal.

Assume H1: finite X.

Apply SNoS_E2 ω omega_ordinal (h (s X)) (Lh (s X) (Ls X HX) (Lsfin X H1)) to the current goal.

Assume HhsX1: SNoLev (h (s X)) ∈ ω.

Assume HhsX2: ordinal (SNoLev (h (s X))).

Assume HhsX3: SNo (h (s X)).

Assume HhsX4: SNo_ (SNoLev (h (s X))) (h (s X)).

We will prove (if finite X then h (s X) + 1 else if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y.

Apply If_i_1 (finite X) (h (s X) + 1) (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) H1 (λ_ u ⇒ u = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y) to the current goal.

We will prove h (s X) + 1 = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y.

Apply xm (finite Y) to the current goal.

Assume H2: finite Y.

Apply SNoS_E2 ω omega_ordinal (h (s Y)) (Lh (s Y) (Ls Y HY) (Lsfin Y H2)) to the current goal.

Assume HhsY1: SNoLev (h (s Y)) ∈ ω.

Assume HhsY2: ordinal (SNoLev (h (s Y))).

Assume HhsY3: SNo (h (s Y)).

Assume HhsY4: SNo_ (SNoLev (h (s Y))) (h (s Y)).

Apply If_i_1 (finite Y) (h (s Y) + 1) (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) H2 (λ_ u ⇒ h (s X) + 1 = u → X = Y) to the current goal.

We will prove h (s X) + 1 = h (s Y) + 1 → X = Y.

Assume H3: h (s X) + 1 = h (s Y) + 1.

Apply Lsinj to the current goal.

We will prove s X = s Y.

An exact proof term for the current goal is Lhinj (s X) (Ls X HX) (s Y) (Ls Y HY) (add_SNo_cancel_R (h (s X)) 1 (h (s Y)) HhsX3 SNo_1 HhsY3 H3).

Assume H2: infinite Y.

Apply xm (finite (ω ∖ Y)) to the current goal.

Assume H3: finite (ω ∖ Y).

Assume H4: h (s X) + 1 = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)).

Apply SNoS_E2 ω omega_ordinal (h (s (ω ∖ Y))) (Lh (s (ω ∖ Y)) (Ls (ω ∖ Y) LoY) (Lsfin (ω ∖ Y) H3)) to the current goal.

Assume HhsY1: SNoLev (h (s (ω ∖ Y))) ∈ ω.

Assume HhsY2: ordinal (SNoLev (h (s (ω ∖ Y)))).

Assume HhsY3: SNo (h (s (ω ∖ Y))).

Assume HhsY4: SNo_ (SNoLev (h (s (ω ∖ Y)))) (h (s (ω ∖ Y))).

We prove the intermediate claim LhsXmhsY: h (s X) + 1 = - h (s (ω ∖ Y)).

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

Use transitivity with and (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)).

An exact proof term for the current goal is If_i_0 (finite Y) (h (s Y) + 1) (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) H2.

An exact proof term for the current goal is If_i_1 (finite (ω ∖ Y)) (- h (s (ω ∖ Y))) (SNoCut (L Y) (R Y)) H3.

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLt_tra 0 (h (s X)) 0 SNo_0 HhsX3 SNo_0 to the current goal.

We will prove 0 < h (s X).

Apply Lh0pos to the current goal.

We will prove s X ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is HX.

We will prove 0 ∈ s X.

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ X}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

We will prove h (s X) < 0.

We prove the intermediate claim LhsXhsX1: h (s X) < h (s X) + 1.

An exact proof term for the current goal is add_SNo_0R (h (s X)) HhsX3 (λu _ ⇒ u < h (s X) + 1) (add_SNo_Lt2 (h (s X)) 0 1 HhsX3 SNo_0 SNo_1 SNoLt_0_1).

We prove the intermediate claim LhsX10: h (s X) + 1 < 0.

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

We will prove - h (s (ω ∖ Y)) < 0.

We prove the intermediate claim LhsYpos: - 0 < h (s (ω ∖ Y)).

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

Apply Lh0pos to the current goal.

We will prove s (ω ∖ Y) ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is LoY.

We will prove 0 ∈ s (ω ∖ Y).

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ ω ∖ Y}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

An exact proof term for the current goal is minus_SNo_Lt_contra1 0 (h (s (ω ∖ Y))) SNo_0 HhsY3 LhsYpos.

An exact proof term for the current goal is SNoLt_tra (h (s X)) (h (s X) + 1) 0 HhsX3 (SNo_add_SNo (h (s X)) 1 HhsX3 SNo_1) SNo_0 LhsXhsX1 LhsX10.

Assume H3: infinite (ω ∖ Y).

Assume H4: h (s X) + 1 = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)).

We prove the intermediate claim LhsXSLRY: h (s X) + 1 = SNoCut (L Y) (R Y).

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

Use transitivity with and (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)).

An exact proof term for the current goal is If_i_0 (finite Y) (h (s Y) + 1) (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) H2.

An exact proof term for the current goal is If_i_0 (finite (ω ∖ Y)) (- h (s (ω ∖ Y))) (SNoCut (L Y) (R Y)) H3.

We will prove False.

Apply SNoLt_irref 1 to the current goal.

We will prove 1 < 1.

Apply SNoLt_tra 1 (h (s X) + 1) 1 SNo_1 (SNo_add_SNo (h (s X)) 1 HhsX3 SNo_1) SNo_1 to the current goal.

We will prove 1 < h (s X) + 1.

We prove the intermediate claim LhsXpos: 0 < h (s X).

Apply Lh0pos to the current goal.

We will prove s X ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is HX.

We will prove 0 ∈ s X.

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ X}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

rewrite the current goal using add_SNo_0L 1 SNo_1 (from right to left) at position 1.

We will prove 0 + 1 < h (s X) + 1.

An exact proof term for the current goal is add_SNo_Lt1 0 1 (h (s X)) SNo_0 SNo_1 HhsX3 LhsXpos.

We will prove h (s X) + 1 < 1.

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

An exact proof term for the current goal is L_R_lt1 Y.

Assume H1: infinite X.

Apply If_i_0 (finite X) (h (s X) + 1) (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) H1 (λ_ u ⇒ u = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y) to the current goal.

We will prove (if finite (ω ∖ X) then - h (s (ω ∖ X)) else SNoCut (L X) (R X)) = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y.

Apply xm (finite (ω ∖ X)) to the current goal.

Assume H2: finite (ω ∖ X).

Apply SNoS_E2 ω omega_ordinal (h (s (ω ∖ X))) (Lh (s (ω ∖ X)) (Ls (ω ∖ X) LoX) (Lsfin (ω ∖ X) H2)) to the current goal.

Assume HhsX1: SNoLev (h (s (ω ∖ X))) ∈ ω.

Assume HhsX2: ordinal (SNoLev (h (s (ω ∖ X)))).

Assume HhsX3: SNo (h (s (ω ∖ X))).

Assume HhsX4: SNo_ (SNoLev (h (s (ω ∖ X)))) (h (s (ω ∖ X))).

Apply If_i_1 (finite (ω ∖ X)) (- h (s (ω ∖ X))) (SNoCut (L X) (R X)) H2 (λ_ u ⇒ u = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y) to the current goal.

We will prove (- h (s (ω ∖ X))) = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y.

Apply xm (finite Y) to the current goal.

Assume H3: finite Y.

Assume H4: (- h (s (ω ∖ X))) = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)).

Apply SNoS_E2 ω omega_ordinal (h (s Y)) (Lh (s Y) (Ls Y HY) (Lsfin Y H3)) to the current goal.

Assume HhsY1: SNoLev (h (s Y)) ∈ ω.

Assume HhsY2: ordinal (SNoLev (h (s Y))).

Assume HhsY3: SNo (h (s Y)).

Assume HhsY4: SNo_ (SNoLev (h (s Y))) (h (s Y)).

We prove the intermediate claim LmhsXhsY: - h (s (ω ∖ X)) = h (s Y) + 1.

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

An exact proof term for the current goal is If_i_1 (finite Y) (h (s Y) + 1) (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) H3.

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLt_tra 0 (h (s Y) + 1) 0 SNo_0 (SNo_add_SNo (h (s Y)) 1 HhsY3 SNo_1) SNo_0 to the current goal.

We will prove 0 < h (s Y) + 1.

We prove the intermediate claim LhsYpos: 0 < h (s Y).

We will prove 0 < h (s Y).

Apply Lh0pos to the current goal.

We will prove s Y ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is HY.

We will prove 0 ∈ s Y.

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ Y}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

An exact proof term for the current goal is SNoLt_tra 0 (h (s Y)) (h (s Y) + 1) SNo_0 HhsY3 (SNo_add_SNo (h (s Y)) 1 HhsY3 SNo_1) LhsYpos (add_SNo_0R (h (s Y)) HhsY3 (λu _ ⇒ u < h (s Y) + 1) (add_SNo_Lt2 (h (s Y)) 0 1 HhsY3 SNo_0 SNo_1 SNoLt_0_1)).

We will prove h (s Y) + 1 < 0.

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

We will prove - h (s (ω ∖ X)) < 0.

We prove the intermediate claim LhsXpos: - 0 < h (s (ω ∖ X)).

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

Apply Lh0pos to the current goal.

We will prove s (ω ∖ X) ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is LoX.

We will prove 0 ∈ s (ω ∖ X).

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ ω ∖ X}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

An exact proof term for the current goal is minus_SNo_Lt_contra1 0 (h (s (ω ∖ X))) SNo_0 HhsX3 LhsXpos.

Assume H3: infinite Y.

Apply If_i_0 (finite Y) (h (s Y) + 1) (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) H3 (λ_ u ⇒ - h (s (ω ∖ X)) = u → X = Y) to the current goal.

We will prove (- h (s (ω ∖ X))) = (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y.

Apply xm (finite (ω ∖ Y)) to the current goal.

Assume H4: finite (ω ∖ Y).

Apply SNoS_E2 ω omega_ordinal (h (s (ω ∖ Y))) (Lh (s (ω ∖ Y)) (Ls (ω ∖ Y) (PowerI ω (ω ∖ Y) (setminus_Subq ω Y))) (Lsfin (ω ∖ Y) H4)) to the current goal.

Assume HhsY1: SNoLev (h (s (ω ∖ Y))) ∈ ω.

Assume HhsY2: ordinal (SNoLev (h (s (ω ∖ Y)))).

Assume HhsY3: SNo (h (s (ω ∖ Y))).

Assume HhsY4: SNo_ (SNoLev (h (s (ω ∖ Y)))) (h (s (ω ∖ Y))).

Apply If_i_1 (finite (ω ∖ Y)) (- h (s (ω ∖ Y))) (SNoCut (L Y) (R Y)) H4 (λ_ u ⇒ - h (s (ω ∖ X)) = u → X = Y) to the current goal.

Assume H5: - h (s (ω ∖ X)) = - h (s (ω ∖ Y)).

We will prove X = Y.

We prove the intermediate claim LoXoY: ω ∖ X = ω ∖ Y.

Apply Lsinj to the current goal.

We will prove s (ω ∖ X) = s (ω ∖ Y).

Apply Lhinj (s (ω ∖ X)) (Ls (ω ∖ X) LoX) (s (ω ∖ Y)) (Ls (ω ∖ Y) LoY) to the current goal.

We will prove h (s (ω ∖ X)) = h (s (ω ∖ Y)).

Use transitivity with - - h (s (ω ∖ X)), and - - h (s (ω ∖ Y)).

Use symmetry.

An exact proof term for the current goal is minus_SNo_invol (h (s (ω ∖ X))) HhsX3.

Use f_equal.

An exact proof term for the current goal is H5.

An exact proof term for the current goal is minus_SNo_invol (h (s (ω ∖ Y))) HhsY3.

We will prove X = Y.

Apply set_ext to the current goal.

Let u be given.

Assume HuX: u ∈ X.

Apply dneg to the current goal.

Assume HuY: u ∉ Y.

Apply setminusE2 ω X u to the current goal.

We will prove u ∈ ω ∖ X.

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

We will prove u ∈ ω ∖ Y.

Apply setminusI to the current goal.

We will prove u ∈ ω.

An exact proof term for the current goal is LX u HuX.

An exact proof term for the current goal is HuY.

We will prove u ∈ X.

An exact proof term for the current goal is HuX.

Let u be given.

Assume HuY: u ∈ Y.

Apply dneg to the current goal.

Assume HuX: u ∉ X.

Apply setminusE2 ω Y u to the current goal.

We will prove u ∈ ω ∖ Y.

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

We will prove u ∈ ω ∖ X.

Apply setminusI to the current goal.

We will prove u ∈ ω.

An exact proof term for the current goal is LY u HuY.

An exact proof term for the current goal is HuX.

We will prove u ∈ Y.

An exact proof term for the current goal is HuY.

Assume H4: infinite (ω ∖ Y).

Apply If_i_0 (finite (ω ∖ Y)) (- h (s (ω ∖ Y))) (SNoCut (L Y) (R Y)) H4 (λ_ u ⇒ - h (s (ω ∖ X)) = u → X = Y) to the current goal.

Assume H5: - h (s (ω ∖ X)) = SNoCut (L Y) (R Y).

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLt_tra 0 (- h (s (ω ∖ X))) 0 SNo_0 (SNo_minus_SNo (h (s (ω ∖ X))) HhsX3) SNo_0 to the current goal.

We will prove 0 < - h (s (ω ∖ X)).

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

An exact proof term for the current goal is L_R_pos Y.

We will prove - h (s (ω ∖ X)) < 0.

We prove the intermediate claim LhsXpos: - 0 < h (s (ω ∖ X)).

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

Apply Lh0pos to the current goal.

We will prove s (ω ∖ X) ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is LoX.

We will prove 0 ∈ s (ω ∖ X).

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ ω ∖ X}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

An exact proof term for the current goal is minus_SNo_Lt_contra1 0 (h (s (ω ∖ X))) SNo_0 HhsX3 LhsXpos.

Assume H2: infinite (ω ∖ X).

Apply If_i_0 (finite (ω ∖ X)) (- h (s (ω ∖ X))) (SNoCut (L X) (R X)) H2 (λ_ u ⇒ u = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y) to the current goal.

We will prove (SNoCut (L X) (R X)) = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y.

Apply xm (finite Y) to the current goal.

Assume H3: finite Y.

Assume H4: SNoCut (L X) (R X) = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)).

Apply SNoS_E2 ω omega_ordinal (h (s Y)) (Lh (s Y) (Ls Y HY) (Lsfin Y H3)) to the current goal.

Assume HhsY1: SNoLev (h (s Y)) ∈ ω.

Assume HhsY2: ordinal (SNoLev (h (s Y))).

Assume HhsY3: SNo (h (s Y)).

Assume HhsY4: SNo_ (SNoLev (h (s Y))) (h (s Y)).

We prove the intermediate claim LLRXhsY: SNoCut (L X) (R X) = h (s Y) + 1.

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

An exact proof term for the current goal is If_i_1 (finite Y) (h (s Y) + 1) (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) H3.

We will prove False.

Apply SNoLt_irref 1 to the current goal.

We will prove 1 < 1.

Apply SNoLt_tra 1 (h (s Y) + 1) 1 SNo_1 (SNo_add_SNo (h (s Y)) 1 HhsY3 SNo_1) SNo_1 to the current goal.

We will prove 1 < h (s Y) + 1.

We prove the intermediate claim LhsYpos: 0 < h (s Y).

Apply Lh0pos to the current goal.

We will prove s Y ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is HY.

We will prove 0 ∈ s Y.

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ Y}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

rewrite the current goal using add_SNo_0L 1 SNo_1 (from right to left) at position 1.

We will prove 0 + 1 < h (s Y) + 1.

An exact proof term for the current goal is add_SNo_Lt1 0 1 (h (s Y)) SNo_0 SNo_1 HhsY3 LhsYpos.

We will prove h (s Y) + 1 < 1.

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

An exact proof term for the current goal is L_R_lt1 X.

Assume H3: infinite Y.

We will prove (SNoCut (L X) (R X)) = (if finite Y then h (s Y) + 1 else if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) → X = Y.

Apply If_i_0 (finite Y) (h (s Y) + 1) (if finite (ω ∖ Y) then - h (s (ω ∖ Y)) else SNoCut (L Y) (R Y)) H3 (λ_ u ⇒ SNoCut (L X) (R X) = u → X = Y) to the current goal.

Apply xm (finite (ω ∖ Y)) to the current goal.

Assume H4: finite (ω ∖ Y).

Apply SNoS_E2 ω omega_ordinal (h (s (ω ∖ Y))) (Lh (s (ω ∖ Y)) (Ls (ω ∖ Y) (PowerI ω (ω ∖ Y) (setminus_Subq ω Y))) (Lsfin (ω ∖ Y) H4)) to the current goal.

Assume HhsY1: SNoLev (h (s (ω ∖ Y))) ∈ ω.

Assume HhsY2: ordinal (SNoLev (h (s (ω ∖ Y)))).

Assume HhsY3: SNo (h (s (ω ∖ Y))).

Assume HhsY4: SNo_ (SNoLev (h (s (ω ∖ Y)))) (h (s (ω ∖ Y))).

Apply If_i_1 (finite (ω ∖ Y)) (- h (s (ω ∖ Y))) (SNoCut (L Y) (R Y)) H4 (λ_ u ⇒ SNoCut (L X) (R X) = u → X = Y) to the current goal.

Assume H5: SNoCut (L X) (R X) = - h (s (ω ∖ Y)).

We will prove False.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

Apply SNoLt_tra 0 (- h (s (ω ∖ Y))) 0 SNo_0 (SNo_minus_SNo (h (s (ω ∖ Y))) HhsY3) SNo_0 to the current goal.

We will prove 0 < - h (s (ω ∖ Y)).

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

An exact proof term for the current goal is L_R_pos X.

We will prove - h (s (ω ∖ Y)) < 0.

We prove the intermediate claim LhsYpos: - 0 < h (s (ω ∖ Y)).

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

Apply Lh0pos to the current goal.

We will prove s (ω ∖ Y) ∈ 𝒫 ω.

Apply Ls to the current goal.

An exact proof term for the current goal is LoY.

We will prove 0 ∈ s (ω ∖ Y).

We will prove 0 ∈ {0} ∪ {ordsucc n|n ∈ ω ∖ Y}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

An exact proof term for the current goal is minus_SNo_Lt_contra1 0 (h (s (ω ∖ Y))) SNo_0 HhsY3 LhsYpos.

Assume H4: infinite (ω ∖ Y).

Apply If_i_0 (finite (ω ∖ Y)) (- h (s (ω ∖ Y))) (SNoCut (L Y) (R Y)) H4 (λ_ u ⇒ SNoCut (L X) (R X) = u → X = Y) to the current goal.

Assume H5: SNoCut (L X) (R X) = SNoCut (L Y) (R Y).

We will prove X = Y.

Apply set_ext to the current goal.

Let n be given.

Assume HnX: n ∈ X.

Apply L_R_inj X LX Y LY H5 (ordsucc n) (nat_ordsucc n (omega_nat_p n (LX n HnX))) to the current goal.

Assume _.

Assume H6: ∀i ∈ ordsucc n, i ∈ X ↔ i ∈ Y.

Apply H6 n (ordsuccI2 n) to the current goal.

Assume H7: n ∈ X → n ∈ Y.

Assume _.

An exact proof term for the current goal is H7 HnX.

Let n be given.

Assume HnY: n ∈ Y.

Apply L_R_inj X LX Y LY H5 (ordsucc n) (nat_ordsucc n (omega_nat_p n (LY n HnY))) to the current goal.

Assume _.

Assume H6: ∀i ∈ ordsucc n, i ∈ X ↔ i ∈ Y.

Apply H6 n (ordsuccI2 n) to the current goal.

Assume _.

Assume H7: n ∈ Y → n ∈ X.

An exact proof term for the current goal is H7 HnY.