proposition: Lemma Exercise1_22E r r' X X': order r -> order r' -> open_o r X -> open_o r' X' -> open_o (order_product2 r r') (X \times X').
proof: Proof. move=> or or' oX oX'; split. rewrite order_product2_sr //. apply: setX_Slr; [ by case: oX | by case: oX']. move=> x y xp /order_product2_P; move=> [_ yp [le1 le2]]. move: oX oX' => [_ ox][_ oy]. move: xp yp => /setX_P [px Px Qy] /setX_P [py _ _]; apply /setX_P;split => //. apply: (ox _ _ Px le1). apply: (oy _ _ Qy le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)