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