proposition: Lemma vctleq_anti : antisymmetric vctleq.
proof: Proof. move=> v1 v2 /andP[/vctleqP[Hsz12 H12] /vctleqP[_ H21]]. apply (eq_from_nth Hsz12 (x0 := 0)) => i _. by apply anti_leq; rewrite H12 H21. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype