proposition: Lemma acomps_cons K H s : acomps K (H :: s) -> acomps H s.
proof: Proof. by case/andP => /= ls; case/andP=> _ p; rewrite /acomps ls. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)