proposition: Lemma mxOver_scalarE S c : (n > 0)%N -> (c%:M \is a @mxOver n n R S) = ((n > 1) ==> (0 \in S)) && (c \in S).
proof: Proof. case: n => [|[|k]]//= _. by apply/mxOverP/idP => [/(_ ord0 ord0)|cij i j]; rewrite ?mxE ?ord1. apply/mxOverP/andP => [cij|[S0 cij] i j]; last by rewrite !mxE; case: eqP. by split; [have := cij 0 1|have := cij 0 0]; rewrite !mxE. 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)