Apply SNo_ind to the current goal.
Let L and R be given.
Assume HLR: SNoCutP L R.
Assume IHL: ∀x ∈ L, - - x = x.
Assume IHR: ∀y ∈ R, - - y = y.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
We prove the intermediate claim LCLR: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R HLR.
We prove the intermediate claim LmCLR: SNo (- SNoCut L R).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LCLR.
We prove the intermediate claim LmmCLR: SNo (- - SNoCut L R).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LmCLR.
We prove the intermediate claim L1: SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R) ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
Apply SNoCutP_SNoCut_fst to the current goal.
An exact proof term for the current goal is HLR.
We will prove SNo (- - SNoCut L R).
An exact proof term for the current goal is LmmCLR.
We will prove ∀x ∈ L, x < - - SNoCut L R.
Let x be given.
Assume Hx.
rewrite the current goal using IHL x Hx (from right to left).
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is HLR1 x Hx.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Lx.
We will prove - - x < - - SNoCut L R.
Apply minus_SNo_Lt_contra (- SNoCut L R) (- x) LmCLR Lmx to the current goal.
We will prove - SNoCut L R < - x.
Apply minus_SNo_Lt_contra x (SNoCut L R) Lx LCLR to the current goal.
We will prove x < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R HLR x Hx.
We will prove ∀y ∈ R, - - SNoCut L R < y.
Let y be given.
Assume Hy.
rewrite the current goal using IHR y Hy (from right to left).
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is HLR2 y Hy.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Ly.
We will prove - - SNoCut L R < - - y.
Apply minus_SNo_Lt_contra (- y) (- SNoCut L R) Lmy LmCLR to the current goal.
We will prove - y < - SNoCut L R.
Apply minus_SNo_Lt_contra (SNoCut L R) y LCLR Ly to the current goal.
We will prove SNoCut L R < y.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R HLR y Hy.
Apply L1 to the current goal.
Assume L1a: SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R).
Assume L1b: SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
We will prove - - SNoCut L R = SNoCut L R.
Use symmetry.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is LCLR.
An exact proof term for the current goal is LmmCLR.
We will prove SNoLev (SNoCut L R) = SNoLev (- - SNoCut L R).
Apply set_ext to the current goal.
We will prove SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R).
An exact proof term for the current goal is L1a.
We will prove SNoLev (- - SNoCut L R) ⊆ SNoLev (SNoCut L R).
Apply Subq_tra (SNoLev (- - SNoCut L R)) (SNoLev (- SNoCut L R)) (SNoLev (SNoCut L R)) to the current goal.
We will prove SNoLev (- - SNoCut L R) ⊆ SNoLev (- SNoCut L R).
Apply minus_SNo_Lev_lem2 (- SNoCut L R) LmCLR to the current goal.
We will prove SNoLev (- SNoCut L R) ⊆ SNoLev (SNoCut L R).
Apply minus_SNo_Lev_lem2 (SNoCut L R) LCLR to the current goal.
We will prove SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
An exact proof term for the current goal is L1b.
∎