proposition: Lemma quo_mx_irr : mx_irreducible rGH <-> mx_irreducible rG.
proof: Proof. split; case/mx_irrP=> n_gt0 irrG; apply/mx_irrP; split=> // U modU; by apply: irrG; rewrite mxmodule_quo in modU *. 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)