proposition: Lemma index_sdprodr G A B M : A ><| B = G -> M \subset B -> #|B : M| = #|G : A <*> M|.
proof: Proof. move=> defG; case/sdprodP: defG (defG) => [[K H -> ->] mulKH nKH _] defG sMH. rewrite -!divgS //=; last by rewrite -genM_join gen_subG -mulKH mulgS. by rewrite -(sdprod_card defG) -(sdprod_card (sdprod_subr defG sMH)) divnMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)