Let L and R be given.
Assume HLR: SNoCutP L R.
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.
Set Lm to be the term {- z|z ∈ R}.
Set Rm to be the term {- w|w ∈ L}.
We will prove (∀w ∈ Lm, SNo w) ∧ (∀z ∈ Rm, SNo z) ∧ (∀w ∈ Lm, ∀z ∈ Rm, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ Lm.
We will prove SNo w.
Apply ReplE_impred R (λz ⇒ - z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume Hwz: w = - z.
rewrite the current goal using Hwz (from left to right).
We will prove SNo (- z).
Apply SNo_minus_SNo to the current goal.
Apply HLR2 to the current goal.
An exact proof term for the current goal is Hz.
Let z be given.
Assume Hz: z ∈ Rm.
We will prove SNo z.
Apply ReplE_impred L (λw ⇒ - w) z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume Hzw: z = - w.
rewrite the current goal using Hzw (from left to right).
We will prove SNo (- w).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is HLR1 w Hw.
Let w be given.
Assume Hw: w ∈ Lm.
Let z be given.
Assume Hz: z ∈ Rm.
Apply ReplE_impred R (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ R.
Assume Hwu: w = - u.
Apply ReplE_impred L (λw ⇒ - w) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ L.
Assume Hzv: z = - v.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
rewrite the current goal using Hzv (from left to right).
We will prove - u < - v.
Apply minus_SNo_Lt_contra v u (HLR1 v Hv) (HLR2 u Hu) to the current goal.
We will prove v < u.
An exact proof term for the current goal is HLR3 v Hv u Hu.
∎