proposition: Lemma count_pos_in : forall a (l: list A), countIn a l > 0 -> exists a', eqA a a' /\ In a' l.
proof: Proof. induction l; simpl. intro w; lia. destruct (eqA_dec a a0). intros _. exists a0; auto. intro w. destruct (IHl w) as [a' [aa' a'l]]. exists a'; auto. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)