The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

Hello,

I'm finding the following theorem difficult, and wonder if anyone could offer
guidance or solution:

  Theorem fin_list : forall n (l : list (fin n)), NoDup l -> length l <= n.

I started by induction on "NoDup l", but I'm not sure how to relate length l
and fin n.  I arrive here:

  n : nat
  x : fin n
  l : list (fin n)
  H : ~ In x l
  H0 : NoDup l
  IHNoDup : length l <= n
  ============================
   length (x :: l) <= n

We should know that length l < n, because a member of the set is not present,
but I can't see a way to derive this fact.

Thanks,
  John