```
Require Import List.
Theorem aux n L (H: forall x, x < n -> In x L) (H0: length L = n): NoDup L.
```

It feels harder than the previous one (How to approach this (seemingly) simple theorem?). Or maybe I lack creativity/cleverness to imagine correct intermediate lemmas.

Can someone give hints? I tried doing induction on n, but I’m missing something.

Deduce by `H0`

that in fact `[0; ...; n-1] = L`

.

Is it “Permutation (seq 0 n) L”? Thank you for the help.

nojb
#4
Yes, absolutely! Look at `NoDup_Permutation_bis`

from the standard library.

Cheers,

Nicolás

1 Like

By the way, there is apparently a problem with this statement in the standard library: no need for the `NoDup l'`

hypothesis (Issue #12119).

1 Like