proposition: Lemma vctminPr v1 v2 : size v1 = size v2 -> vctmin v1 v2 <=V v2.
proof: Proof. move=> Hsz; apply/vctleqP. rewrite size_vctmin Hsz minnn; split; first by []. move=> i; rewrite nth_vctmin. exact: geq_minr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype