proposition: Lemma vctleq_trans : transitive vctleq.
proof: Proof. move=> v2 v1 v3 /vctleqP[Hsz12 H12] /vctleqP[Hsz23 H23]. apply/vctleqP; rewrite Hsz12; split; first by []. by move=> i; exact: leq_trans (H12 i) (H23 i). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype