proposition: Lemma mxOver_diagE (S : {pred R}) k (D : 'rV[R]_k) : k > 0 -> (diag_mx D \is a mxOver S) = ((k > 1) ==> (0 \in S)) && (D \is a mxOver S).
proof: Proof. case: k => [|[|k]]//= in D * => _. by rewrite [diag_mx _]mx11_scalar [D in RHS]mx11_scalar !mxE. apply/idP/andP => [/mxOverP DS|[S0 DS]]; last exact: mxOver_diag. split; first by have /[!mxE] := DS 0 1. by apply/mxOverP => i j; have := DS j j; rewrite ord1 !mxE eqxx. 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)