proposition: Lemma p_eltM_norm pi x y : x \in 'N(<[y]>) -> pi.-elt x -> pi.-elt y -> pi.-elt (x * y).
proof: Proof. move=> nyx pi_x pi_y; apply: (@mem_p_elt pi _ (<[x]> <*> <[y]>)%G). by rewrite /= norm_joinEl ?cycle_subG // pgroupM; apply/andP. by rewrite groupM // mem_gen // inE cycle_id ?orbT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)