proposition: Lemma metacyclic_sol G : metacyclic G -> solvable G.
proof: Proof. case/metacyclicP=> K [cycK nsKG cycGq]. by rewrite (series_sol nsKG) !abelian_sol ?cyclic_abelian. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)