proposition: Lemma mxOver_diag (S : {pred R}) k (D : 'rV[R]_k) : 0 \in S -> D \is a mxOver S -> diag_mx D \is a mxOver S.
proof: Proof. move=> S0 DS; apply/mxOverP => i j; rewrite !mxE. by case: eqP => //; rewrite (mxOverP DS). 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)