proposition: Lemma diag_mxP n (A : 'M[V]_n) : reflect (exists d : 'rV_n, A = diag_mx d) (is_diag_mx A).
proof: Proof. apply: (iffP (is_diag_mxP A)) => [Adiag|[d ->] i j neq_ij]; last first. by rewrite !mxE -val_eqE (negPf neq_ij). exists (\row_i A i i); apply/matrixP => i j; rewrite !mxE. by case: (altP (i =P j)) => [->|/Adiag->]. 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)