proposition: Lemma trivg_acomps K s : acomps K s -> (K :==: 1) = (s == [::]).
proof: Proof. case/andP=> ls cs; apply/eqP/eqP; last first. by move=> se; rewrite se /= in ls; apply/eqP. move=> G1; case: s ls cs => // H s _ /=; case/andP; case/maxgroupP. by rewrite G1 sub1G andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)