proposition: Lemma rsim_abelem_subg : mx_rsim rHG rH.
proof: Proof. exists 1%:M => // [|x Hx]; first by rewrite row_free_unit unitmx1. by rewrite mul1mx mulmx1 eq_abelem_subg_repr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient gproduct action finalg) mathcomp(zmodp commutator cyclic center pgroup gseries) mathcomp(nilpotent sylow maximal abelian matrix) mathcomp(mxalgebra mxrepresentation)