We will prove simply_ordered_set Sbar_Omega.

We will prove Sbar_Omega = R ∨ Sbar_Omega = rational_numbers ∨ Sbar_Omega = ω ∨ Sbar_Omega = ω ∖ {0} ∨ Sbar_Omega = setprod 2 ω ∨ Sbar_Omega = setprod R R ∨ ordinal Sbar_Omega.

Apply orIR to the current goal.

An exact proof term for the current goal is Sbar_Omega_ordinal.

∎