proposition: Lemma index_quotient_ker : K \subset G -> G \subset 'N(H) -> (#|G / H : K / H| * #|G :&: H : K|)%N = #|G : K|.
proof: Proof. by rewrite -{5}(ker_coset H); apply: index_morphim_ker. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)