Let z be given.

Assume Hz: z ∈ SNoL (- x).

Apply SNoL_E (- x) Lmx z Hz to the current goal.

Assume Hz1: SNo z.

rewrite the current goal using minus_SNo_Lev x Hx (from left to right).

Assume Hz2: SNoLev z ∈ SNoLev x.

Assume Hz3: z < - x.

We will prove z ∈ {- w|w ∈ SNoR x}.

rewrite the current goal using minus_SNo_invol z Hz1 (from right to left).

Apply ReplI to the current goal.

We will prove - z ∈ SNoR x.

Apply SNoR_I x Hx (- z) (SNo_minus_SNo z Hz1) to the current goal.

We will prove SNoLev (- z) ∈ SNoLev x.

rewrite the current goal using minus_SNo_Lev z Hz1 (from left to right).

An exact proof term for the current goal is Hz2.

We will prove x < - z.

Apply minus_SNo_Lt_contra2 z x Hz1 Hx to the current goal.

An exact proof term for the current goal is Hz3.

Let z be given.

Assume Hz: z ∈ {- w|w ∈ SNoR x}.

Apply ReplE_impred (SNoR x) minus_SNo z Hz to the current goal.

Let w be given.

Assume Hw: w ∈ SNoR x.

Assume Hzw: z = - w.

We will prove z ∈ SNoL (- x).

rewrite the current goal using Hzw (from left to right).

We will prove - w ∈ SNoL (- x).

Apply SNoR_E x Hx w Hw to the current goal.

Assume Hw1: SNo w.

Assume Hw2: SNoLev w ∈ SNoLev x.

Assume Hw3: x < w.

Apply SNoL_I (- x) Lmx (- w) (SNo_minus_SNo w Hw1) to the current goal.

We will prove SNoLev (- w) ∈ SNoLev (- x).

rewrite the current goal using minus_SNo_Lev w Hw1 (from left to right).

rewrite the current goal using minus_SNo_Lev x Hx (from left to right).

An exact proof term for the current goal is Hw2.

We will prove - w < - x.

Apply minus_SNo_Lt_contra x w Hx Hw1 to the current goal.

An exact proof term for the current goal is Hw3.