Let L1, R1, L2 and R2 be given.
Assume HLR1 HLR2.
Assume H1: ∀w ∈ L1, w < SNoCut L2 R2.
Assume H2: ∀z ∈ R1, SNoCut L2 R2 < z.
Assume H3: ∀w ∈ L2, w < SNoCut L1 R1.
Assume H4: ∀z ∈ R2, SNoCut L1 R1 < z.
We prove the intermediate claim LNLR1: SNo (SNoCut L1 R1).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L1 R1 HLR1.
We prove the intermediate claim LNLR2: SNo (SNoCut L2 R2).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L2 R2 HLR2.
Apply SNoLe_antisym (SNoCut L1 R1) (SNoCut L2 R2) LNLR1 LNLR2 to the current goal.
We will prove SNoCut L1 R1 ≤ SNoCut L2 R2.
An exact proof term for the current goal is SNoCut_Le L1 R1 L2 R2 HLR1 HLR2 H1 H4.
We will prove SNoCut L2 R2 ≤ SNoCut L1 R1.
An exact proof term for the current goal is SNoCut_Le L2 R2 L1 R1 HLR2 HLR1 H3 H2.
∎