proposition: Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : (1%:M \in R)%MS -> reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R).
proof: Proof. case: (posnP n) => [-> | n_gt0] in R *; set S := mxvec _ => sSR. by rewrite [R]thinmx0 mxrank0; right; case; rewrite /is_scalar_mx ?insubF. have rankS: \rank S = 1%N. apply/eqP; rewrite eqn_leq rank_leq_row lt0n mxrank_eq0 mxvec_eq0. by rewrite -mxrank_eq0 mxrank1 -lt0n. rewrite -{2}rankS (ltn_leqif (mxrank_leqif_sup sSR)). apply: (iffP idP) => [/row_subPn[i] | [A sAR]]. rewrite -[row i R]vec_mxK memmx1; set A := vec_mx _ => nsA. by exists A; rewrite // vec_mxK row_sub. by rewrite -memmx1; apply/contra/submx_trans. 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 finalg zmodp matrix)