We will prove simply_ordered_set (setprod R R).

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

Apply orIL to the current goal.

Apply orIR to the current goal.

Use reflexivity.

∎