Let alpha be given.

Assume Ha.

Let z be given.

Assume Hz: SNo z.

Assume H1: SNoLev z ∈ ordsucc alpha.

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 alpha.

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 - alpha ≤ z.

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

We will prove - alpha ≤ - - z.

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

We will prove - z ≤ alpha.

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

∎