proposition: Lemma vctminC: commutative vctmin.
proof: Proof. move=> v1 v2. apply (eq_from_nth (x0 := 0)); first by rewrite !size_vctmin minnC. by move=> i Hi; rewrite !nth_vctmin minnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype