We will prove simply_ordered_set R.

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

Apply orIL to the current goal.

Apply orIL to the current goal.

Apply orIL to the current goal.

Apply orIL to the current goal.

Apply orIL to the current goal.

Apply orIL to the current goal.

Use reflexivity.

∎