proposition: Lemma vctleqP v1 v2 : reflect (size v1 = size v2 /\ forall i, nth 0 v1 i <= nth 0 v2 i) (v1 <=V v2).
proof: Proof. rewrite /vctleq; apply (iffP andP). - move=> [/eqP Hsz /allP/= Hleq]; split; first by []. move=> i; case: (ltnP i (size (zip v1 v2))). + by move=> /(mem_nth (0, 0))/Hleq; rewrite !nth_zip. + rewrite size_zip Hsz minnn => Hi. by rewrite !nth_default ?Hsz. - move=> [Hsz Hall]; rewrite Hsz; split; first by []. apply/allP => /= [[a b]] Hin. have:= nth_index (0, 0) Hin; move: Hin; rewrite -index_mem. move: (index _ _) => i /=. rewrite size_zip Hsz minnn => Hi. rewrite nth_zip //= => [] [<- <-]. exact: Hall. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype