proposition: Lemma vctminP v1 v2 v : v <=V v1 -> v <=V v2 -> v <=V (vctmin v1 v2).
proof: Proof. move=> /vctleqP[Hsz1 Hv1] /vctleqP[Hsz2 Hv2]. apply/vctleqP; rewrite size_vctmin -Hsz1 -Hsz2 minnn; split; first by []. by move=> i; rewrite nth_vctmin leq_min Hv1 Hv2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype