proposition: Lemma coprime_p'group p K R : coprime #|K| #|R| -> p.-group R -> R :!=: 1 -> p^'.-group K.
proof: Proof. move=> coKR pR ntR; have [p_pr _ [e oK]] := pgroup_pdiv pR ntR. by rewrite oK coprime_sym coprime_pexpl // prime_coprime // -p'natE in coKR. 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)