proposition: Lemma order_product2_preorder f g: preorder f -> preorder g -> preorder (prod_of_relation f g).
proof: Proof. move => [_ rf tf] [_ rg tg]; apply: preorder_from_rel; hnf; split. move => x y z[pxy qxy][pyz qyz]. split; [ apply: tf pxy pyz | apply: tg qxy qyz]. move=> x y [pxy qxy]; split; split; try apply: rf; try apply: rg; substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)