[STATEMENT]
lemma successive_ends_1:
  "successive P xs \<Longrightarrow> \<not> P x \<Longrightarrow> successive P ys \<Longrightarrow> successive P (xs @ x # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>successive P xs; \<not> P x; successive P ys\<rbrakk> \<Longrightarrow> successive P (xs @ x # ys)
[PROOF STEP]
by (induction _ xs rule: list_two_induct) (fastforce intro: successive_stepI)+