We will prove ordered_square ⊆ setprod R R.

We prove the intermediate claim Hsq: ordered_square = setprod unit_interval unit_interval.

Use reflexivity.

rewrite the current goal using Hsq (from left to right).

An exact proof term for the current goal is (setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R).

∎