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.