proposition: Lemma mxdirect_delta n f : {in P &, injective f} -> mxdirect (\sum_(i | P i) <<delta_mx 0 (f i) : 'rV[F]_n>>).
proof: Proof. pose fP := image f P => Uf; have UfP: uniq fP by apply/dinjectiveP. suffices /mxdirectP : mxdirect (\sum_i <<delta_mx 0 i : 'rV[F]_n>>). rewrite /= !(bigID [in fP] predT) -!big_uniq //= !big_map !big_enum. by move/mxdirectP; rewrite mxdirect_addsE => /andP[]. apply/mxdirectP=> /=; transitivity (mxrank (1%:M : 'M[F]_n)). apply/eqmx_rank; rewrite submx1 mx1_sum_delta summx_sub_sums // => i _. by rewrite -(mul_delta_mx (0 : 'I_1)) genmxE submxMl. rewrite mxrank1 -[LHS]card_ord -sum1_card. by apply/eq_bigr=> i _; rewrite /= mxrank_gen mxrank_delta. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)