proposition: Lemma index_injm G H : 'injm f -> G \subset D -> #|f @* G : f @* H| = #|G : H|.
proof: Proof. move=> injf dG; rewrite -{2}(setIidPr dG) -(indexgI _ H) /=. rewrite -index_morphim_ker ?subsetIl ?subsetIr //= setIAC morphimIdom setIC. rewrite injmI ?subsetIr // indexgI /= morphimIdom setIC ker_injm //. by rewrite -(indexgI (1 :&: _)) /= -setIA !(setIidPl (sub1G _)) indexgg muln1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)