proposition: Lemma order_product2_sr f g: order f -> order g -> substrate (prod_of_relation f g) = (substrate f) \times (substrate g).
proof: Proof. move=> orf og; apply: order_product2_sr1; by apply: order_preorder. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)