Apply ordinal_binunion to the current goal.

Apply ordinal_famunion to the current goal.

Let w be given.

Assume Hw.

We will prove ordinal (ordsucc (SNoLev w)).

Apply ordinal_ordsucc to the current goal.

We will prove ordinal (SNoLev w).

Apply SNoLev_ordinal to the current goal.

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

Apply ordinal_famunion to the current goal.

Let z be given.

Assume Hz.

We will prove ordinal (ordsucc (SNoLev z)).

Apply ordinal_ordsucc to the current goal.

We will prove ordinal (SNoLev z).

Apply SNoLev_ordinal to the current goal.

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

Apply ordinal_ordsucc_In_Subq (ordsucc ω) ordsucc_omega_ordinal ((⋃_{w ∈ L}ordsucc (SNoLev w)) ∪ (⋃_{z ∈ R}ordsucc (SNoLev z))) to the current goal.

We will prove ((⋃_{w ∈ L}ordsucc (SNoLev w)) ∪ (⋃_{z ∈ R}ordsucc (SNoLev z))) ∈ ordsucc ω.

Apply ordinal_In_Or_Subq ((⋃_{w ∈ L}ordsucc (SNoLev w)) ∪ (⋃_{z ∈ R}ordsucc (SNoLev z))) (ordsucc ω) Lo ordsucc_omega_ordinal to the current goal.

Assume H6.

An exact proof term for the current goal is H6.

Assume H6: ordsucc ω ⊆ (⋃_{w ∈ L}ordsucc (SNoLev w)) ∪ (⋃_{z ∈ R}ordsucc (SNoLev z)).

We will prove False.

Apply binunionE (⋃_{w ∈ L}ordsucc (SNoLev w)) (⋃_{z ∈ R}ordsucc (SNoLev z)) ω (H6 ω (ordsuccI2 ω)) to the current goal.

Assume H7: ω ∈ ⋃_{w ∈ L}ordsucc (SNoLev w).

Apply famunionE_impred L (λw ⇒ ordsucc (SNoLev w)) ω H7 to the current goal.

Let w be given.

Assume Hw: w ∈ L.

Assume H8: ω ∈ ordsucc (SNoLev w).

Apply SNoS_E2 ω omega_ordinal w (HL w Hw) to the current goal.

Assume Hw1: SNoLev w ∈ ω.

We will prove False.

Apply ordsuccE (SNoLev w) ω H8 to the current goal.

Assume H9: ω ∈ SNoLev w.

An exact proof term for the current goal is In_no2cycle ω (SNoLev w) H9 Hw1.

Assume H9: ω = SNoLev w.

We will prove False.

Apply In_irref ω to the current goal.

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

An exact proof term for the current goal is Hw1.

Assume H7: ω ∈ ⋃_{z ∈ R}ordsucc (SNoLev z).

Apply famunionE_impred R (λz ⇒ ordsucc (SNoLev z)) ω H7 to the current goal.

Let z be given.

Assume Hz: z ∈ R.

Assume H8: ω ∈ ordsucc (SNoLev z).

Apply SNoS_E2 ω omega_ordinal z (HR z Hz) to the current goal.

Assume Hz1: SNoLev z ∈ ω.

We will prove False.

Apply ordsuccE (SNoLev z) ω H8 to the current goal.

Assume H9: ω ∈ SNoLev z.

An exact proof term for the current goal is In_no2cycle ω (SNoLev z) H9 Hz1.

Assume H9: ω = SNoLev z.

We will prove False.

Apply In_irref ω to the current goal.

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

An exact proof term for the current goal is Hz1.

Assume H6: SNoLev x ∈ ω.

We will prove x ∈ real.

Apply SNoS_omega_real to the current goal.

We will prove x ∈ SNoS_ ω.

Apply SNoS_I ω omega_ordinal x (SNoLev x) H6 to the current goal.

We will prove SNo_ (SNoLev x) x.

Apply SNoLev_ to the current goal.

An exact proof term for the current goal is H1.

Assume H6: SNoLev x = ω.

We will prove x ∈ real.

Apply real_I to the current goal.

We will prove x ∈ SNoS_ (ordsucc ω).

Apply SNoS_I (ordsucc ω) ordsucc_omega_ordinal x (SNoLev x) to the current goal.

We will prove SNoLev x ∈ ordsucc ω.

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

Apply ordsuccI2 to the current goal.

We will prove SNo_ (SNoLev x) x.

Apply SNoLev_ to the current goal.

An exact proof term for the current goal is H1.

Assume H7: x = ω.

Apply HR0 to the current goal.

Apply Empty_eq to the current goal.

Let z be given.

Assume Hz: z ∈ R.

Apply SNoLt_irref z to the current goal.

We will prove z < z.

Apply SNoLt_tra z x z (HLR2 z Hz) H1 (HLR2 z Hz) to the current goal.

We will prove z < x.

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

We will prove z < ω.

Apply ordinal_SNoLev_max ω omega_ordinal z (HLR2 z Hz) to the current goal.

We will prove SNoLev z ∈ ω.

Apply SNoS_E2 ω omega_ordinal z (HR z Hz) to the current goal.

Assume Hz1: SNoLev z ∈ ω.

Assume _ _ _.

An exact proof term for the current goal is Hz1.

We will prove x < z.

Apply H4 to the current goal.

An exact proof term for the current goal is Hz.

Assume H7: x = - ω.

Apply HL0 to the current goal.

Apply Empty_eq to the current goal.

Let w be given.

Assume Hw: w ∈ L.

Apply SNoLt_irref w to the current goal.

We will prove w < w.

Apply SNoLt_tra w x w (HLR1 w Hw) H1 (HLR1 w Hw) to the current goal.

We will prove w < x.

Apply H3 to the current goal.

An exact proof term for the current goal is Hw.

We will prove x < w.

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

We will prove - ω < w.

Apply minus_SNo_Lt_contra1 w ω (HLR1 w Hw) SNo_omega to the current goal.

We will prove - w < ω.

Apply ordinal_SNoLev_max ω omega_ordinal (- w) (SNo_minus_SNo w (HLR1 w Hw)) to the current goal.

We will prove SNoLev (- w) ∈ ω.

rewrite the current goal using minus_SNo_Lev w (HLR1 w Hw) (from left to right).

Apply SNoS_E2 ω omega_ordinal w (HL w Hw) to the current goal.

Assume Hw1: SNoLev w ∈ ω.

Assume _ _ _.

An exact proof term for the current goal is Hw1.

Let q be given.

Assume Hq: q ∈ SNoS_ ω.

Assume H7: ∀k ∈ ω, abs_SNo (q + - x) < eps_ k.

We will prove False.

Apply SNoS_E2 ω omega_ordinal q Hq to the current goal.

Assume Hq1: SNoLev q ∈ ω.

Assume Hq2: ordinal (SNoLev q).

Assume Hq3: SNo q.

Assume Hq4: SNo_ (SNoLev q) q.

We prove the intermediate claim LqL: ∀w ∈ L, w < q.

Let w be given.

Assume Hw: w ∈ L.

Apply SNoLtLe_or w q (HLR1 w Hw) Hq3 to the current goal.

Assume H8: w < q.

An exact proof term for the current goal is H8.

Assume H8: q ≤ w.

We will prove False.

Apply HL1 w Hw to the current goal.

Let w' be given.

Assume H.

Apply H to the current goal.

Assume H9: w' ∈ L.

Assume H10: w < w'.

We prove the intermediate claim LqL1: w' + - q ∈ SNoS_ ω.

Apply add_SNo_SNoS_omega to the current goal.

An exact proof term for the current goal is HL w' H9.

Apply minus_SNo_SNoS_omega to the current goal.

An exact proof term for the current goal is Hq.

Apply SNoS_E2 ω omega_ordinal (w' + - q) LqL1 to the current goal.

Assume Hw'q1: SNoLev (w' + - q) ∈ ω.

Assume Hw'q2: ordinal (SNoLev (w' + - q)).

Assume Hw'q3: SNo (w' + - q).

Assume Hw'q4: SNo_ (SNoLev (w' + - q)) (w' + - q).

We prove the intermediate claim LqL2: 0 < w' + - q.

Apply SNoLt_minus_pos q w' Hq3 (HLR1 w' H9) to the current goal.

We will prove q < w'.

An exact proof term for the current goal is SNoLeLt_tra q w w' Hq3 (HLR1 w Hw) (HLR1 w' H9) H8 H10.

Set k to be the term SNoLev (w' + - q).

We prove the intermediate claim LqL3: w' + - q ∈ SNoS_ (ordsucc k).

An exact proof term for the current goal is SNoS_I (ordsucc k) (ordinal_ordsucc k (nat_p_ordinal k (omega_nat_p k Hw'q1))) (w' + - q) k (ordsuccI2 k) Hw'q4.

We prove the intermediate claim Lek: SNo (eps_ k).

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

We prove the intermediate claim LqL4: eps_ k < w' + - q.

An exact proof term for the current goal is SNo_pos_eps_Lt k (omega_nat_p k Hw'q1) (w' + - q) LqL3 LqL2.

Apply SNoLt_irref (eps_ k) to the current goal.

Apply SNoLt_tra (eps_ k) (w' + - q) (eps_ k) Lek Hw'q3 Lek LqL4 to the current goal.

We will prove w' + - q < eps_ k.

We prove the intermediate claim Lxq: SNo (x + - q).

An exact proof term for the current goal is SNo_add_SNo x (- q) H1 (SNo_minus_SNo q Hq3).

Apply SNoLt_tra (w' + - q) (x + - q) (eps_ k) Hw'q3 Lxq Lek to the current goal.

We will prove w' + - q < x + - q.

Apply add_SNo_Lt1 w' (- q) x (HLR1 w' H9) (SNo_minus_SNo q Hq3) H1 to the current goal.

We will prove w' < x.

Apply H3 to the current goal.

We will prove w' ∈ L.

An exact proof term for the current goal is H9.

We will prove x + - q < eps_ k.

Apply SNoLtLe_or (x + - q) 0 Lxq SNo_0 to the current goal.

Assume H11: x + - q < 0.

An exact proof term for the current goal is SNoLt_tra (x + - q) 0 (eps_ k) Lxq SNo_0 Lek H11 (SNo_eps_pos k Hw'q1).

Assume H11: 0 ≤ x + - q.

rewrite the current goal using nonneg_abs_SNo (x + - q) H11 (from right to left).

We will prove abs_SNo (x + - q) < eps_ k.

rewrite the current goal using abs_SNo_dist_swap x q H1 Hq3 (from left to right).

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

We prove the intermediate claim LqR: ∀z ∈ R, q < z.

Let z be given.

Assume Hz: z ∈ R.

Apply SNoLtLe_or q z Hq3 (HLR2 z Hz) to the current goal.

Assume H8: q < z.

An exact proof term for the current goal is H8.

Assume H8: z ≤ q.

We will prove False.

Apply HR1 z Hz to the current goal.

Let z' be given.

Assume H.

Apply H to the current goal.

Assume H9: z' ∈ R.

Assume H10: z' < z.

We prove the intermediate claim LqR1: q + - z' ∈ SNoS_ ω.

Apply add_SNo_SNoS_omega to the current goal.

An exact proof term for the current goal is Hq.

Apply minus_SNo_SNoS_omega to the current goal.

An exact proof term for the current goal is HR z' H9.

Apply SNoS_E2 ω omega_ordinal (q + - z') LqR1 to the current goal.

Assume Hz'q1: SNoLev (q + - z') ∈ ω.

Assume Hz'q2: ordinal (SNoLev (q + - z')).

Assume Hz'q3: SNo (q + - z').

Assume Hz'q4: SNo_ (SNoLev (q + - z')) (q + - z').

We prove the intermediate claim LqR2: 0 < q + - z'.

Apply SNoLt_minus_pos z' q (HLR2 z' H9) Hq3 to the current goal.

We will prove z' < q.

An exact proof term for the current goal is SNoLtLe_tra z' z q (HLR2 z' H9) (HLR2 z Hz) Hq3 H10 H8.

Set k to be the term SNoLev (q + - z').

We prove the intermediate claim LqR3: q + - z' ∈ SNoS_ (ordsucc k).

An exact proof term for the current goal is SNoS_I (ordsucc k) (ordinal_ordsucc k (nat_p_ordinal k (omega_nat_p k Hz'q1))) (q + - z') k (ordsuccI2 k) Hz'q4.

We prove the intermediate claim Lek: SNo (eps_ k).

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

We prove the intermediate claim LqR4: eps_ k < q + - z'.

An exact proof term for the current goal is SNo_pos_eps_Lt k (omega_nat_p k Hz'q1) (q + - z') LqR3 LqR2.

Apply SNoLt_irref (eps_ k) to the current goal.

Apply SNoLt_tra (eps_ k) (q + - z') (eps_ k) Lek Hz'q3 Lek LqR4 to the current goal.

We will prove q + - z' < eps_ k.

We prove the intermediate claim Lxq: SNo (q + - x).

An exact proof term for the current goal is SNo_add_SNo q (- x) Hq3 (SNo_minus_SNo x H1).

Apply SNoLt_tra (q + - z') (q + - x) (eps_ k) Hz'q3 Lxq Lek to the current goal.

We will prove q + - z' < q + - x.

Apply add_SNo_Lt2 q (- z') (- x) Hq3 (SNo_minus_SNo z' (HLR2 z' H9)) (SNo_minus_SNo x H1) to the current goal.

We will prove - z' < - x.

Apply minus_SNo_Lt_contra x z' H1 (HLR2 z' H9) to the current goal.

We will prove x < z'.

Apply H4 to the current goal.

We will prove z' ∈ R.

An exact proof term for the current goal is H9.

We will prove q + - x < eps_ k.

Apply SNoLtLe_or (q + - x) 0 Lxq SNo_0 to the current goal.

Assume H11: q + - x < 0.

An exact proof term for the current goal is SNoLt_tra (q + - x) 0 (eps_ k) Lxq SNo_0 Lek H11 (SNo_eps_pos k Hz'q1).

Assume H11: 0 ≤ q + - x.

rewrite the current goal using nonneg_abs_SNo (q + - x) H11 (from right to left).

We will prove abs_SNo (q + - x) < eps_ k.

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

Apply H5 q Hq3 LqL LqR to the current goal.

Assume H10: SNoLev x ⊆ SNoLev q.

We will prove False.

Apply In_irref (SNoLev q) to the current goal.

Apply H10 to the current goal.

We will prove SNoLev q ∈ SNoLev x.

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

An exact proof term for the current goal is Hq1.