proposition: Lemma countIn_nth : forall a (l: list A), countIn a l > 0 -> exists p, exists a', eqA a a' /\ nth_error l p = Some a'.
proof: Proof. induction l. simpl; intros; lia. simpl; intros. destruct (eqA_dec a a0). exists 0; exists a0. split; trivial. destruct IHl as [p [a' [aa' lpa']]]; trivial. exists (S p); exists a'; split; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)