proposition: Lemma exists_mem_of_count_pos : forall P l, count P l > 0 -> exists x, mem x l /\ P x.
proof: Proof. Proof using. introv. rewrite* count_pos_eq_exists_mem. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)