proposition: Lemma count_pos_eq_exists_mem : forall P l, (count P l > 0) = (exists x, mem x l /\ P x).
proof: Proof. Proof using. intros. rewrite <- Exists_eq_count_pos, Exists_eq_exists_mem. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)