proposition: Lemma ker_cprodm : 'ker cprodm = [set a * b^-1 | a in H, b in K & fH a == fK b].
proof: Proof. rewrite ker_restrm (setIidPr _) ?subIset ?ker_pprodm //; apply/orP; left. by case/cprodP: eqHK_G => _ <- cHK; rewrite cent_joinEr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)