Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal beta.
Set Lo1 to be the term {x + beta|x ∈ SNoS_ alpha}.
Set Lo2 to be the term {alpha + x|x ∈ SNoS_ beta}.
We will prove alpha + beta = SNoCut (Lo1 ∪ Lo2) Empty.
We prove the intermediate claim La: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim Lb: SNo beta.
An exact proof term for the current goal is ordinal_SNo beta Hb.
rewrite the current goal using add_SNo_eq alpha La beta Lb (from left to right).
We will prove SNoCut ({x + beta|x ∈ SNoL alpha} ∪ {alpha + x|x ∈ SNoL beta}) ({x + beta|x ∈ SNoR alpha} ∪ {alpha + x|x ∈ SNoR beta}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using ordinal_SNoL alpha Ha (from left to right).
rewrite the current goal using ordinal_SNoL beta Hb (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) ({x + beta|x ∈ SNoR alpha} ∪ {alpha + x|x ∈ SNoR beta}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using ordinal_SNoR alpha Ha (from left to right).
rewrite the current goal using ordinal_SNoR beta Hb (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) ({x + beta|x ∈ Empty} ∪ {alpha + x|x ∈ Empty}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using Repl_Empty (from left to right).
rewrite the current goal using Repl_Empty (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) (Empty ∪ Empty) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using binunion_idl (from left to right).
Use reflexivity.
∎