proposition: Lemma Vanmx_antimE : Vanmx = antim [::].
proof: Proof. Proof using. by apply/matrixP => i j /=; rewrite !mxE nth_default. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition mathcomp(matrix)