proposition: Lemma sub_seqprod_lexi d (T : porderType disp) : subrel (<=%O : rel (seqprod_with d T)) (<=%O : rel (seq T)).
proof: Proof. elim=> [|x1 s1 ihs1] [|x2 s2]//=; rewrite le_cons lexi_cons /=. by move=> /andP[-> /ihs1->]; rewrite implybT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)