proposition: Lemma mxring_idP m n (R : 'A_(m, n)) : reflect (exists e, mxring_id R e) (has_mxring_id R).
proof: Proof. apply: (iffP andP) => [[nzR] | [e [nz_e Re ideR idRe]]]. case/submxP=> v; rewrite -[v]vec_mxK; move/vec_mx: v => e. rewrite !mul_mx_row; case/eq_row_mx => /eqP. rewrite eq_sym -submxE => Re. case/eq_row_mx; rewrite !{1}mul_rV_lin1 /= mxvecK. set u := (_ *m _) => /(can_inj mxvecK) idRe /(can_inj mxvecK) ideR. exists e; split=> // [ | A /submxP[a defA] | A /submxP[a defA]]. - by apply: contra nzR; rewrite ideR => /eqP->; rewrite !linear0. - by rewrite -{2}[A]mxvecK defA idRe mulmxA mx_rV_lin -defA /= mxvecK. by rewrite -{2}[A]mxvecK defA ideR mulmxA mx_rV_lin -defA /= mxvecK. split. by apply: contraNneq nz_e => R0; rewrite R0 eqmx0 in Re; rewrite (memmx0 Re). apply/submxP; exists (mxvec e); rewrite !mul_mx_row !{1}mul_rV_lin1. rewrite submxE in Re; rewrite {Re}(eqP Re). congr (row_mx 0 (row_mx (mxvec _) (mxvec _))); apply/row_matrixP=> i. by rewrite !row_mul !mul_rV_lin1 /= mxvecK ideR vec_mxK ?row_sub. by rewrite !row_mul !mul_rV_lin1 /= mxvecK idRe vec_mxK ?row_sub. 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)