proposition: Lemma index_morphim_ker G H : H \subset G -> G \subset D -> (#|f @* G : f @* H| * #|'ker_G f : H|)%N = #|G : H|.
proof: Proof. move=> sHG sGD; apply/eqP. rewrite -(eqn_pmul2l (cardG_gt0 (f @* H))) mulnA Lagrange ?morphimS //. rewrite !card_morphim (setIidPr sGD) (setIidPr (subset_trans sHG sGD)). rewrite -(eqn_pmul2l (cardG_gt0 ('ker_H f))) /=. by rewrite -{1}(setIidPr sHG) setIAC mulnCA mulnC mulnA !LagrangeI Lagrange. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)