Definition eq_dec A := forall (x y: A), { x = y } + { x <> y }.
Definition index_error A (dec: eq_dec A) (x: A) (L: list A): option nat.
Proof.
induction L.
+ exact None.
+ destruct (dec x a).
- exact (Some 0).
- exact (match IHL with Some n => Some (S n) | None => None end).
Defined.
Definition index A (dec: eq_dec A) (default: nat) (x: A) (L: list A): nat :=
match (index_error dec x L) with
| Some n => n
| None => default
end.

Why do I think it would be nice to have? It is kind of inverse function of â€śnthâ€ť and seems useful for me anyway.
So, Iâ€™m collecting interesting/useful lemmas to prove about it. If you have any suggestions, feel free to post them.

Also, Iâ€™m trying to prove that

Theorem index_of_list_elements A (dec: eq_dec A) (d: nat) (L: list A) (H: NoDup L): map (fun i => index dec d i L) L = seq 0 (length L).

I know itâ€™s possible, because I have done it once already (but then the .v file become gibberish a day later - maybe electricity was lost in a bad moment or smth - and I hadnâ€™t saved it with version control software so it was lost and this time I have no success).
If anyone has any hints, I will be very grateful.

Concerning the original question about index, it looks indeed natural in a context of lists on types with decidable equality.
As first key statements, I would start with your argument of being an inverse for nth: index (nth ...) = ... and nth (index ...) = ....
By the way, I would recommend to keep consistency with respect to nth on the order of arguments by putting the default element as the last one for index.
A possibly interesting and related function would collect the list of indices:

Fixpoint indices A (dec: eq_dec A) x l :=
match l with
| nil => nil
| y :: tl => if dec x y then 0 :: map S (indices A dec x tl)
else map S (indices A dec x tl)
end.

In case if someone wants to have fun, there are two other (unproven, but tested to be true) theorems:

Definition is_perm n L := Permutation L (seq 0 n).
Theorem T1 n x (H: is_perm n x):
map (fun i => nth i (map (fun i0 => index Nat.eq_dec i0 x 0) (seq 0 n)) 0) x = seq 0 n.
Proof. Admitted.
Theorem T2 n x x0 x1 (H: is_perm n x) (H0: is_perm n x0) (H1: is_perm n x1):
map (fun i : nat => nth i (map (fun i0 : nat => nth i0 x 0) x0) 0) x1 =
map (fun i : nat => nth (nth i x0 0) x 0) x1.
Proof. Admitted.

T1 corresponds to multiplication of inverse permutation with original permutation (which gives identity permutation), and T2 corresponds to associativity of permutation multiplication.
[Edit:] I have proven T1 now.

I believe that in this case direct approach is impossible (for T2 and for me) and it is necessary to prove correspondence with differently defined notion of permutation, prove its properties and transfer back to this definition. That is, permutations as bijections.
[Edit:] I have proven T2 too, even if it feels like a bit of black magic.