The solution by @nojb is probably the most conceptual one by using also seq and in_seq from the standard library.

You can prove it also by induction on n (with L generalized) and then rely on the following results from the standard library: in_split and NoDup_remove.

I made proof using @olaure01’s suggestion. Soon I will try @nojb’s approach too, for training purposes.

Definition permutation_list n := { L: list nat | (forall x, In x L <-> x < n) /\ NoDup L }.
Theorem permutation_list_length n (p: permutation_list n): length (proj1_sig p) = n.
Proof.
destruct p as [L [H H0]]. simpl. revert L H H0. induction n.
+ intros. destruct L; auto. simpl in *. assert (n < 0) by (apply H; auto). inversion H1.
+ intros. assert (In n L) by (apply H; auto). destruct (in_split n L H1) as [L1 [L2 H2]].
subst. apply NoDup_remove in H0. destruct H0 as [H0 H2].
assert (forall x, In x (L1 ++ L2) <-> x < n).
- intuition.
* destruct (H x) as [H4 H5]. assert (In x (L1 ++ n :: L2)).
{ apply in_or_app. simpl. apply in_app_or in H3. tauto. }
pose (H4 H6) as H7. inversion H7. subst. tauto. auto.
* assert (x < S n) by intuition. apply H in H4.
apply in_app_or in H4. simpl in H4. destruct H4 as [H4 | [H5 | H6]].
++ apply in_or_app; auto.
++ omega.
++ apply in_or_app; auto.
- apply IHn in H3; auto. rewrite app_length. simpl. rewrite app_length in H3. omega.
Qed.

I would use a slightly different solution relying on library functions:

Theorem permutation_list_length
n l (H: forall x, (x \in l) = (x < n)) (H0: uniq l): size l = n.
Proof.
have hl : iota 0 n =i l by move=> x; rewrite mem_iota H.
by have/esym/eqP := uniq_size_uniq (iota_uniq 0 n) hl; rewrite H0 size_iota.
Qed.

“From mathcomp Require Import all_ssreflect.”, right?
I haven’t started studying SSReflect and MathComp library yet. I’ve planned to do that some day, though.

Definitely will look at development suggested by olaure01.
I’ve made github repository too, although it’s a bit messy right now. Please ignore the slightly ambitious name of it.