Let α be given.

Assume Ha.

Let z be given.

Assume Hz: SNo z.

Assume H1: SNoLev z ∈ ordsucc α.

We prove the intermediate claim Lz1: SNo (- z).

An exact proof term for the current goal is SNo_minus_SNo z Hz.

We prove the intermediate claim Lz2: SNoLev (- z) ∈ ordsucc α.

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

An exact proof term for the current goal is H1.

We will prove - α ≤ z.

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

We will prove - α ≤ - - z.

Apply minus_SNo_Le_contra (- z) α Lz1 (ordinal_SNo α Ha) to the current goal.

We will prove - z ≤ α.

An exact proof term for the current goal is ordinal_SNoLev_max_2 α Ha (- z) Lz1 Lz2.

∎