proposition: Lemma trivg_comps G s : comps G s -> (G :==: 1) = (s == [::]).
proof: Proof. case/andP=> ls cs; apply/eqP/eqP=> [G1 | s1]; last first. by rewrite s1 /= in ls; apply/eqP. by case: s {ls} cs => //= H s /andP[/maxgroupp]; rewrite G1 /proper 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)