Apply SNoLev_ind to the current goal.
Let v be given.
Assume Hv: SNo v.
Assume IHv: ∀u ∈ SNoS_ (SNoLev v), ∀L R, SNoCutP L R → u = SNoCut L R → - u = SNoCut {- z|z ∈ R} {- w|w ∈ L}.
Let L and R be given.
Assume HLR: SNoCutP L R.
Apply HLR to the current goal.
Assume HLR1.
Apply HLR1 to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
Assume HvLR: v = SNoCut L R.
Set mL to be the term {- w|w ∈ L}.
Set mR to be the term {- z|z ∈ R}.
Set mLv to be the term {- w|w ∈ SNoL v}.
Set mRv to be the term {- z|z ∈ SNoR v}.
We prove the intermediate claim L1: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R HLR.
We prove the intermediate claim L2: SNoCutP mR mL.
An exact proof term for the current goal is minus_SNo_SNoCutP_gen L R HLR.
Apply SNoCutP_SNoCut_impred mR mL L2 to the current goal.
Assume H1: SNo (SNoCut mR mL).
Assume H2: SNoLev (SNoCut mR mL) ∈ ordsucc ((⋃x ∈ mRordsucc (SNoLev x)) ∪ (⋃y ∈ mLordsucc (SNoLev y))).
Assume H3: ∀x ∈ mR, x < SNoCut mR mL.
Assume H4: ∀y ∈ mL, SNoCut mR mL < y.
Assume H5: ∀z, SNo z → (∀x ∈ mR, x < z) → (∀y ∈ mL, z < y) → SNoLev (SNoCut mR mL) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) z.
We prove the intermediate claim L3: ∀x ∈ mR, x < - v.
Let x be given.
Assume Hx: x ∈ mR.
Apply ReplE_impred R minus_SNo x Hx to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume Hxz: x = - z.
We will prove x < - v.
rewrite the current goal using Hxz (from left to right).
We will prove - z < - v.
Apply minus_SNo_Lt_contra v z Hv (HLR2 z Hz) to the current goal.
We will prove v < z.
rewrite the current goal using HvLR (from left to right).
We will prove SNoCut L R < z.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R HLR z Hz.
We prove the intermediate claim L4: ∀y ∈ mL, - v < y.
Let y be given.
Assume Hy: y ∈ mL.
Apply ReplE_impred L minus_SNo y Hy to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume Hyw: y = - w.
We will prove - v < y.
rewrite the current goal using Hyw (from left to right).
We will prove - v < - w.
Apply minus_SNo_Lt_contra w v (HLR1 w Hw) Hv to the current goal.
We will prove w < v.
rewrite the current goal using HvLR (from left to right).
We will prove w < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R HLR w Hw.
Apply H5 (- v) (SNo_minus_SNo v Hv) L3 L4 to the current goal.
Assume H6: SNoLev (SNoCut mR mL) ⊆ SNoLev (- v).
Assume H7: SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) (- v).
We prove the intermediate claim L5: ordinal (SNoLev (SNoCut mR mL)).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is H1.
We prove the intermediate claim L6: ordinal (SNoLev (- v)).
Apply SNoLev_ordinal to the current goal.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hv.
Apply ordinal_In_Or_Subq (SNoLev (SNoCut mR mL)) (SNoLev (- v)) L5 L6 to the current goal.
Assume H8: SNoLev (SNoCut mR mL) ∈ SNoLev (- v).
We will prove False.
We prove the intermediate claim L7: SNoCut mR mL ∈ SNoS_ (SNoLev v).
Apply SNoS_I2 to the current goal.
We will prove SNo (SNoCut mR mL).
An exact proof term for the current goal is H1.
We will prove SNo v.
An exact proof term for the current goal is Hv.
We will prove SNoLev (SNoCut mR mL) ∈ SNoLev v.
rewrite the current goal using minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
We prove the intermediate claim LIH: - SNoCut mR mL = SNoCut {- z|z ∈ mL} {- w|w ∈ mR}.
An exact proof term for the current goal is IHv (SNoCut mR mL) L7 mR mL L2 (λq H ⇒ H).
We prove the intermediate claim L8: {- z|z ∈ mL} = L.
Apply Repl_invol_eq (λx ⇒ x ∈ L) minus_SNo to the current goal.
Let x be given.
Assume Hx: x ∈ L.
We will prove - - x = x.
An exact proof term for the current goal is minus_SNo_invol x (HLR1 x Hx).
Let x be given.
Assume Hx: x ∈ L.
An exact proof term for the current goal is Hx.
We prove the intermediate claim L9: {- z|z ∈ mR} = R.
Apply Repl_invol_eq (λy ⇒ y ∈ R) minus_SNo to the current goal.
Let y be given.
Assume Hy: y ∈ R.
We will prove - - y = y.
An exact proof term for the current goal is minus_SNo_invol y (HLR2 y Hy).
Let y be given.
Assume Hy: y ∈ R.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L10: - SNoCut mR mL = v.
rewrite the current goal using LIH (from left to right).
rewrite the current goal using L8 (from left to right).
rewrite the current goal using L9 (from left to right).
Use symmetry.
An exact proof term for the current goal is HvLR.
Apply In_irref (SNoLev v) to the current goal.
We will prove SNoLev v ∈ SNoLev v.
rewrite the current goal using L10 (from right to left) at position 1.
We will prove SNoLev (- SNoCut mR mL) ∈ SNoLev v.
rewrite the current goal using minus_SNo_Lev (SNoCut mR mL) H1 (from left to right).
rewrite the current goal using minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
Assume H8: SNoLev (- v) ⊆ SNoLev (SNoCut mR mL).
We will prove - v = SNoCut mR mL.
Use symmetry.
Apply SNo_eq (SNoCut mR mL) (- v) H1 (SNo_minus_SNo v Hv) to the current goal.
We will prove SNoLev (SNoCut mR mL) = SNoLev (- v).
Apply set_ext to the current goal.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H8.
We will prove SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) (- v).
An exact proof term for the current goal is H7.
∎