proposition: Lemma is_scalar_mxP A : reflect (exists a, A = a%:M) (is_scalar_mx A).
proof: Proof. rewrite /is_scalar_mx; case: insubP => [i _ _ | ]. by apply: (iffP eqP) => [|[a ->]]; [exists (A i i) | rewrite mxE eqxx]. rewrite -eqn0Ngt => /eqP n0; left; exists 0. by rewrite raddf0; rewrite n0 in A *; rewrite [A]flatmx0. 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)