proposition: Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2.
proof: Proof. intros x l; induction l as [|a l IHl]; simpl; [destruct 1|destruct 1 as [?|H]]. - subst a; auto. exists [], l; auto. - destruct (IHl H) as (l1,(l2,H0)). exists (a::l1), l2; simpl. apply f_equal. auto. Qed.
imports: PeanoNat