proposition: Lemma sub_prod_lexi d (T : porderType disp1) (T' : porderType disp2) : subrel (<=%O : rel (T *prod[d] T')) (<=%O : rel (T * T')).
proof: Proof. by case=> [x1 x2] [y1 y2]; rewrite leEprod leEprodlexi /=; case: comparableP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)