[STATEMENT]
lemma dropWhile_Cons: "(dropWhile P xs) = x#ys \<Longrightarrow> \<not> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dropWhile P xs = x # ys \<Longrightarrow> \<not> P x
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dropWhile P [] = x # ys \<Longrightarrow> \<not> P x
 2. \<And>a xs. \<lbrakk>dropWhile P xs = x # ys \<Longrightarrow> \<not> P x; dropWhile P (a # xs) = x # ys\<rbrakk> \<Longrightarrow> \<not> P x
[PROOF STEP]
apply (auto split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done