proposition: Lemma eq_mxdiag (B_ B'_ : forall i, 'M[V]_(p_ i)) : (forall i, B_ i = B'_ i) -> (\mxdiag_i B_ i = \mxdiag_i B'_ i).
proof: Proof. by move=> /eq_mxdiagP. 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)