Pigeonhole principle in Coq

Pigeon.v

Section Pigeon.
  Require Import List.
  Require Import Arith.
  Variable A : Type.

  Definition Unique : list A -> Prop :=
    list_rect _ True (fun x xs hyp => ~(In x xs) /\ hyp).

  Definition Sub (xs ys : list A) : Prop := forall {x}, In x xs -> In x ys.
  
  Lemma remove (x : A) xs (p : In x xs) :
    exists xs', (forall x', x' <> x -> In x' xs -> In x' xs') /\ (length xs = S (length xs')).
  Proof.
    induction xs.
      inversion p.
      destruct p.
        subst a.
        exists xs.
        split.
          intros x' neq pin.
          destruct pin.
            contradict neq. symmetry. assumption.
            assumption.            
          reflexivity.
        destruct (IHxs H) as [xs' pxs']. clear IHxs.
        destruct pxs' as [p1 plen]. rename a into x'.
        exists (x' :: xs').
        split.
          intros x'' neq pin. destruct pin.
            subst x'. left. reflexivity.
            right. apply p1. assumption. assumption.
          simpl.
          rewrite -> plen.
          reflexivity. Qed.

    Theorem pigeon :
      forall xs ys, Sub xs ys -> length ys < length xs -> ~ (Unique xs).
    Proof.
      induction xs.
        intros ys _ plen. inversion plen.
        simpl. intros ys psub plen. intro puniq.
        rename a into x.
        destruct (remove x ys) as [ys' pys']. apply psub. left. reflexivity.
        destruct pys' as [psub' plen'].
        destruct puniq as [x_not_in_xs uniqxs].
        apply (IHxs ys').
          unfold Sub. intros. apply psub'. intro. subst x0. contradict x_not_in_xs. assumption.
          apply psub. right. assumption.
          rewrite plen' in plen.
          apply lt_S_n.
          assumption.
          assumption. Qed.
End Pigeon.