I have this theorem I can’t prove.

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

I’m searching for ideas (intermediate lemmas etc.) that would allow me to prove it. I will try to prove them (lemmas) by myself, as much as possible.