proposition: Lemma in_cprodM : {in setX H K &, {morph in_cprod : u v / u * v}}.
proof: Proof. rewrite /in_cprod /cprod_by; case: cprod_by_key => /= u v Gu Gv. have nkerHKG := normal_norm (sub_center_normal ker_cprod_by_central). by rewrite -!morphM ?mem_quotient // (subsetP nkerHKG). 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)