[STATEMENT]
theorem (in group) trivial_derived_seq_imp_solvable:
  assumes "subgroup H G" and "((derived G) ^^ n) H = { \<one> }" shows "solvable_seq G H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solvable_seq G H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subgroup H G
(derived G ^^ n) H = {\<one>}

goal (1 subgoal):
 1. solvable_seq G H
[PROOF STEP]
proof (induct n arbitrary: H, simp add: unity[of G])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n H. \<lbrakk>\<And>H. \<lbrakk>subgroup H G; (derived G ^^ n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H; subgroup H G; (derived G ^^ Suc n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>subgroup ?H G; (derived G ^^ n) ?H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup H G
(derived G ^^ Suc n) H = {\<one>}

goal (1 subgoal):
 1. \<And>n H. \<lbrakk>\<And>H. \<lbrakk>subgroup H G; (derived G ^^ n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H; subgroup H G; (derived G ^^ Suc n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subgroup ?H G; (derived G ^^ n) ?H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup H G
(derived G ^^ Suc n) H = {\<one>}

goal (1 subgoal):
 1. solvable_seq G H
[PROOF STEP]
using augment_solvable_seq derived_is_subgroup[OF subgroup.subset]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subgroup ?H G; (derived G ^^ n) ?H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup H G
(derived G ^^ Suc n) H = {\<one>}
\<lbrakk>subgroup ?H G; solvable_seq G (derived G ?H)\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup ?H G \<Longrightarrow> subgroup (derived G ?H) G

goal (1 subgoal):
 1. solvable_seq G H
[PROOF STEP]
by (simp add: funpow_swap1)
[PROOF STATE]
proof (state)
this:
solvable_seq G H

goal:
No subgoals!
[PROOF STEP]
qed