proposition: Lemma mxdiagB (B_ B'_ : forall i, 'M[V]_(p_ i)) : \mxdiag_i (B_ i - B'_ i) = \mxdiag_i (B_ i) - \mxdiag_i (B'_ i).
proof: Proof. by rewrite mxdiagD mxdiagN. 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 countalg finalg zmodp)