Require Import PeanoNat.
Require Import List.
Import ListNotations.


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

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).

Theorem t : forall n k, n <= k -> In k (iota n) -> False.
Proof.
intro n; induction n; intros k nlek kin.
- cbn in kin; contradiction.
- cbn in kin; apply app_split in kin.
  + eapply IHn with (k := k).
    * transitivity (S n); eauto.
    * assumption.
  + inversion 1; subst.
    * apply (Nat.nle_succ_diag_l _ nlek).
    * contradiction.
Qed.

Corollary t1 : forall n, In n (iota n) -> False.
intro n; apply (t n n); reflexivity.
Qed.