proposition: Lemma prl_dl3_osr: preorder_on (prl_dl3_or) (I \times L).
proof: Proof. split; first by apply:(order_product2_preorder or prl_dl3_orL). by move:(order_product2_sr1 or prl_dl3_orL); rewrite sr prl_dl3_srL. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)