Let α be given.
Assume Ha: ordinal α.
Let β be given.
Assume Hb: ordinal β.
Set Lo1 to be the term {x + β|x ∈ SNoS_ α}.
Set Lo2 to be the term {α + x|x ∈ SNoS_ β}.
We will prove α + β = SNoCut (Lo1 ∪ Lo2) Empty.
We prove the intermediate claim La: SNo α.
An exact proof term for the current goal is ordinal_SNo α Ha.
We prove the intermediate claim Lb: SNo β.
An exact proof term for the current goal is ordinal_SNo β Hb.
rewrite the current goal using add_SNo_eq α La β Lb (from left to right).
We will prove SNoCut ({x + β|x ∈ SNoL α} ∪ {α + x|x ∈ SNoL β}) ({x + β|x ∈ SNoR α} ∪ {α + x|x ∈ SNoR β}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using ordinal_SNoL α Ha (from left to right).
rewrite the current goal using ordinal_SNoL β Hb (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) ({x + β|x ∈ SNoR α} ∪ {α + x|x ∈ SNoR β}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using ordinal_SNoR α Ha (from left to right).
rewrite the current goal using ordinal_SNoR β Hb (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) ({x + β|x ∈ Empty} ∪ {α + 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.
∎