proposition: Lemma order_product2_or f g: order f -> order g -> order (prod_of_relation f g).
proof: Proof. move=> orf og. have [gr rr tr]: preorder (prod_of_relation f g). by apply: order_product2_preorder; apply: order_preorder. move: orf og => [_ rf tf af] [_ rg tg ag]. split => //. move => x y /Zo_P [pa [pb pc]] /Zo_P [qa [qb qc]]. move: pb pc qb qc; aw => pb pc qb qc. move: pa => /setX_P [_ ]; aw ;move /setX_P => [px _ _] /setX_P [py _ _]. apply: pair_exten => //; [exact: (af _ _ pb qb) | exact: (ag _ _ pc qc)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)