proposition: Lemma injm_sdprod : 'injm f -> K ><| H = G -> f @* K ><| f @* H = f @* G.
proof: Proof. move=> inj_f; case/sdprodP=> _ defG nKH tiKH. by rewrite /sdprod -injmI // tiKH morphim1 subxx morphim_pprod // pprodE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)