proposition: Lemma rsim_regular_factmod : {U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (factmod_repr modU)}}.
proof: Proof. pose v : 'rV[F]_n := nz_row 1%:M. pose fU := lin1_mx (mulmx v \o gring_mx rG); pose U := kermx fU. have modU: mxmodule aG U. apply/mxmoduleP => x Gx; apply/sub_kermxP/row_matrixP=> i. rewrite 2!row_mul row0; move: (row i U) (sub_kermxP (row_sub i U)) => u. by rewrite !mul_rV_lin1 /= gring_mxJ // mulmxA => ->; rewrite mul0mx. have def_n: \rank (cokermx U) = n. apply/eqP; rewrite mxrank_coker mxrank_ker subKn ?rank_leq_row // -genmxE. rewrite -[_ == _]sub1mx; have [_ _ ->] := irrG; rewrite ?submx1 //. rewrite (eqmx_module _ (genmxE _)); apply/mxmoduleP=> x Gx. apply/row_subP=> i; apply: eq_row_sub (gring_index G (enum_val i * x)) _. rewrite !rowE mulmxA !mul_rV_lin1 /= -mulmxA -gring_mxJ //. by rewrite -rowE rowK. rewrite (eqmx_eq0 (genmxE _)); apply/rowV0Pn. exists v; last exact: (nz_row_mxsimple irrG). apply/submxP; exists (gring_row (aG 1%g)); rewrite mul_rV_lin1 /=. by rewrite -gring_opE gring_opG // repr_mx1 mulmx1. exists U; exists modU; apply: mx_rsim_sym. exists (val_factmod 1%:M *m fU) => // [|x Gx]. rewrite /row_free eqn_leq rank_leq_row /= -subn_eq0 -mxrank_ker mxrank_eq0. apply/rowV0P=> u /sub_kermxP; rewrite mulmxA => /sub_kermxP. by rewrite -/U -in_factmod_eq0 mulmxA mulmx1 val_factmodK => /eqP. rewrite mulmxA -val_factmodE (canRL (addKr _) (add_sub_fact_mod U _)). rewrite mulmxDl mulNmx (sub_kermxP (val_submodP _)) oppr0 add0r. apply/row_matrixP=> i; move: (val_factmod _) => zz. by rewrite !row_mul !mul_rV_lin1 /= gring_mxJ // mulmxA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)