proposition: Lemma lePseqprod d d' (T : porderType d) (s1 s2 : seqprod_with d' T) : reflect ((size s1 <= size s2)%N /\ (forall x i, i < size s1 -> nth x s1 i <= nth x s2 i)) (s1 <= s2).
proof: Proof. elim: s1 s2 => [|x s1 IHs] [|y s2] //=; try by constructor; try case. rewrite ltnS leEseq; apply: (iffP idP) => [/andP[lexy /IHs [-> Hs12]]|[? Hs12]]. by split => // ? [] //= i /Hs12. by rewrite (Hs12 x 0%N) //=; apply/IHs; split => // ? i; apply: (Hs12 _ i.+1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)