proposition: Lemma trivgVpdiv G : G :=: 1 \/ (exists2 p, prime p & p %| #|G|).
proof: Proof. have [leG1|lt1G] := leqP #|G| 1; first by left; apply: card_le1_trivg. by right; exists (pdiv #|G|); rewrite ?pdiv_dvd ?pdiv_prime. 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)