proposition: Lemma p_eltM pi x y : commute x y -> pi.-elt x -> pi.-elt y -> pi.-elt (x * y).
proof: Proof. move=> cxy; apply: p_eltM_norm; apply: (subsetP (cent_sub _)). by rewrite cent_gen cent_set1; apply/cent1P. 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)