proposition: Lemma ker_cprod_by_is_group : group_set kerHK.
proof: Proof. apply/group_setP; rewrite inE /= group1 morph1 invg1 /=. split=> // [[x1 y1] [x2 y2]]. rewrite inE /= => /andP[Zx1 /eqP->]; have [_ cGx1] := setIP Zx1. rewrite inE /= => /andP[Zx2 /eqP->]; have [Gx2 _] := setIP Zx2. by rewrite inE /= groupM //= -invMg (centP cGx1) // morphM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)