proposition: Lemma pidl_or: preorder_on (prod_of_relation r1 r2) (I1 \times I2).
proof: Proof. split; first by apply:order_product2_preorder. by move:(order_product2_sr1 or1 or2); rewrite sr1 sr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)