Let L be given.
Assume HL.
Let R be given.
Assume HR.
Assume HLR.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Set x to be the term
SNoCut L R.
Set L_ to be the term
λn ⇒ {w' ∈ SNoS_ n|∃w ∈ L, w' ≤ w} of type
set → set.
Set R_ to be the term
λn ⇒ {z' ∈ SNoS_ n|∃z ∈ R, z ≤ z'} of type
set → set.
Set L' to be the term
⋃n ∈ ωL_ n.
Set R' to be the term
⋃n ∈ ωR_ n.
Set x' to be the term
SNoCut L' R'.
We prove the intermediate
claim LL'L:
∀w' ∈ L', ∃w ∈ L, w' ≤ w.
Let w' be given.
Assume Hw'.
Let n be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ n) (λw' ⇒ ∃w ∈ L, w' ≤ w) w' Hw'2.
We prove the intermediate
claim LR'R:
∀z' ∈ R', ∃z ∈ R, z ≤ z'.
Let z' be given.
Assume Hz'.
Let n be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ n) (λz' ⇒ ∃z ∈ R, z ≤ z') z' Hz'2.
We prove the intermediate
claim LL'o:
L' ⊆ SNoS_ ω.
Let w' be given.
Assume Hw'.
Let n be given.
An exact proof term for the current goal is Hw'6.
We prove the intermediate
claim LR'o:
R' ⊆ SNoS_ ω.
Let z' be given.
Assume Hz'.
Let n be given.
An exact proof term for the current goal is Hz'6.
We prove the intermediate
claim LL':
∀w' ∈ L', SNo w'.
Let w' be given.
Assume Hw'.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim LR':
∀z ∈ R', SNo z.
Let z' be given.
Assume Hz'.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim LLR':
SNoCutP L' R'.
Apply and3I to the current goal.
An exact proof term for the current goal is LL'.
An exact proof term for the current goal is LR'.
Let w' be given.
Assume Hw'.
Let z' be given.
Assume Hz'.
Apply LL'L w' Hw' to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Apply LR'R z' Hz' to the current goal.
Let z be given.
Assume H.
Apply H to the current goal.
Apply SNoLeLt_tra w' w z' (LL' w' Hw') (HLR1 w Hw) (LR' z' Hz') Hw'w to the current goal.
Apply SNoLtLe_tra w z z' (HLR1 w Hw) (HLR2 z Hz) (LR' z' Hz') to the current goal.
Apply HLR3 to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is Hzz'.
We prove the intermediate
claim L1:
∀w ∈ L, ∃w' ∈ L', w ≤ w'.
Let w be given.
Assume Hw.
Apply real_E w (HL w Hw) to the current goal.
Assume _ _ _ _ _.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H6.
Apply SepI to the current goal.
An exact proof term for the current goal is Hw1.
We will
prove ∃u ∈ L, w ≤ u.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
Apply HL1 w Hw to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
Apply real_E w' (HL w' Hw') to the current goal.
Assume _ _ _ _ _.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H7.
Apply SepI to the current goal.
An exact proof term for the current goal is Hw'1.
We will
prove ∃u ∈ L, w' ≤ u.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
An exact proof term for the current goal is Hww'.
Apply SNoLtE w w' Hw1 Hw'1 Hww' to the current goal.
Let w'' be given.
rewrite the current goal using H6 (from left to right).
Assume _ _.
Assume _ _.
We use w'' to witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hw''1.
We will
prove ∃u ∈ L, w'' ≤ u.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
An exact proof term for the current goal is Hw''4.
An exact proof term for the current goal is Hw''3.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
An
exact proof term for the current goal is
In_irref ω H8.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
An
exact proof term for the current goal is
In_irref ω H8.
We prove the intermediate
claim L2:
∀z ∈ R, ∃z' ∈ R', z' ≤ z.
Let z be given.
Assume Hz.
Apply real_E z (HR z Hz) to the current goal.
Assume _ _ _ _ _.
We use z to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H6.
Apply SepI to the current goal.
An exact proof term for the current goal is Hz1.
We will
prove ∃u ∈ R, u ≤ z.
We use z to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz.
Apply HR1 z Hz to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
Apply real_E z' (HR z' Hz') to the current goal.
Assume _ _ _ _ _.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H7.
Apply SepI to the current goal.
An exact proof term for the current goal is Hz'1.
We will
prove ∃u ∈ R, u ≤ z'.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
An exact proof term for the current goal is Hz'z.
Apply SNoLtE z' z Hz'1 Hz1 Hz'z to the current goal.
Let z'' be given.
rewrite the current goal using H7 (from left to right).
Assume _ _.
Assume _ _.
We use z'' to witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hz''1.
We will
prove ∃u ∈ R, u ≤ z''.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
An exact proof term for the current goal is Hz''3.
An exact proof term for the current goal is Hz''4.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
An
exact proof term for the current goal is
In_irref ω H8.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
An
exact proof term for the current goal is
In_irref ω H8.
We prove the intermediate
claim L3:
L' ≠ 0.
Apply HL0 to the current goal.
Let w be given.
Apply L1 w Hw to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
Apply EmptyE w' to the current goal.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hw'.
We prove the intermediate
claim L4:
R' ≠ 0.
Apply HR0 to the current goal.
Let z be given.
Apply L2 z Hz to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
Apply EmptyE z' to the current goal.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hz'.
We prove the intermediate
claim L5:
∀w ∈ L', ∃w' ∈ L', w < w'.
Let w be given.
Assume Hw.
Apply LL'L w Hw to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Apply HL1 u Hu to the current goal.
Let v be given.
Assume H.
Apply H to the current goal.
Apply L1 v Hv to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
Apply SNoLeLt_tra w u w' (LL' w Hw) (HLR1 u Hu) (LL' w' Hw') Hwu to the current goal.
An
exact proof term for the current goal is
SNoLtLe_tra u v w' (HLR1 u Hu) (HLR1 v Hv) (LL' w' Hw') Huv Hvw'.
We prove the intermediate
claim L6:
∀z ∈ R', ∃z' ∈ R', z' < z.
Let z be given.
Assume Hz.
Apply LR'R z Hz to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Apply HR1 u Hu to the current goal.
Let v be given.
Assume H.
Apply H to the current goal.
Apply L2 v Hv to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
Apply SNoLeLt_tra z' v z (LR' z' Hz') (HLR2 v Hv) (LR' z Hz) Hz'v to the current goal.
An
exact proof term for the current goal is
SNoLtLe_tra v u z (HLR2 v Hv) (HLR2 u Hu) (LR' z Hz) Hvu Huz.
We prove the intermediate
claim Lxx':
x = x'.
An exact proof term for the current goal is HLR.
An exact proof term for the current goal is LLR'.
Let w be given.
Apply L1 w Hw to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
An exact proof term for the current goal is HLR1 w Hw.
An exact proof term for the current goal is LL' w' Hw'.
An exact proof term for the current goal is H1'.
An exact proof term for the current goal is Hww'.
Apply H3' to the current goal.
An exact proof term for the current goal is Hw'.
Let z be given.
Apply L2 z Hz to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
An
exact proof term for the current goal is
SNoLtLe_tra x' z' z H1' (LR' z' Hz') (HLR2 z Hz) (H4' z' Hz') Hz'z.
Let w be given.
Apply LL'L w Hw to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
An
exact proof term for the current goal is
SNoLeLt_tra w u x (LL' w Hw) (HLR1 u Hu) H1 Hwu (H3 u Hu).
Let z be given.
Apply LR'R z Hz to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
An
exact proof term for the current goal is
SNoLtLe_tra x u z H1 (HLR2 u Hu) (LR' z Hz) (H4 u Hu) Huz.
rewrite the current goal using Lxx' (from left to right).
∎