Proving increasing iota in Coq

I am stuck on a goal.

Assume we have the following definition:

Fixpoint iota (n : nat) : list nat :=
  match n with
    | 0   => []
    | S k => iota k ++ [k]
  end.

And we want to prove:

Theorem t1 : forall n, In n (iota n) -> False.

So far, I have managed to the following:

Theorem t1 : forall n, In n (iota n) -> False.
Proof.
  intros.
  induction n.
    - cbn in H. contradiction.
    - cbn in H. apply app_split in H.
      Focus 2. unfold not. intros.
      unfold In in H0. destruct H0. assert (~(n = S n)) by now apply s_inj.
      contradiction.
      apply H0.
      apply IHn.

I used these two lemmas, proofs omitted:

Axiom app_split : forall A x (l l2 : list A), In x (l ++ l2) -> not (In x l2) -> In x l.
Axiom s_inj     : forall n, ~(n = S n).

However, I am completely stuck, I need to somehow show that: In n (iota n) assuming In (S n) (iota n).