proposition: Lemma quo_mx_quotient : (E_ rGH :=: E_ rG)%MS.
proof: Proof. apply/eqmxP/andP; split; apply/row_subP=> i. rewrite rowK; case/morphimP: (enum_valP i) => x _ Gx ->{i}. rewrite quo_repr_coset // (eq_row_sub (enum_rank_in Gx x)) // rowK. by rewrite enum_rankK_in. rewrite rowK -(quo_mx_coset krH nHG) ?enum_valP //; set Hx := coset H _. have GHx: Hx \in (G / H)%g by rewrite mem_quotient ?enum_valP. by rewrite (eq_row_sub (enum_rank_in GHx Hx)) // rowK enum_rankK_in. 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)