proposition: Lemma order_product2_sr1 f g: preorder f -> preorder g -> substrate (prod_of_relation f g) = (substrate f) \times (substrate g).
proof: Proof. move=> [_ rf _] [_ rg _ ]; apply: graph_on_sr. move => a /setX_P [pa Ps Qs]. by split; [apply: rf | apply: rg]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)