I prefer to use my own set library. The collections in the Coq library are just too big and too complicated for me. Maybe in a few years.
There is also a library for dsets, decidable sets, for which member ship is decidable.

Section Sets.

  Variable A : Type.


  Definition set : Type := AProp.

  Definition empty_set : set := fun _False.

  Definition full_set : set := fun _True.

  Definition is_full_set(P : set) : Prop := (a : A), P a.

  Definition add(a : A)(P : set) : set := fun(b : A) ⇒ a = b P b.

  Definition subset(P Q : set) : Prop := (a : A), P aQ a.

  Definition union(P Q : set) : set := fun(a : A) ⇒ P a Q a.

  Definition intersection(P Q : set) : set := fun(a : A) ⇒ P a Q a.

  Definition set_inverse(P : set) : set := fun(a : A) ⇒ ¬ (P a).

subset properties

  Lemma subset_refl : (P : set), subset P P.

  Lemma subset_trans : (P1 P2 P3 : set),
    subset P1 P2subset P2 P3subset P1 P3.

  Lemma subset_add : (P : set)(a : A), subset P (add a P).

  Lemma subset_union_left : (P Q : set), subset P (union P Q).

  Lemma subset_union_right : (P Q : set), subset Q (union P Q).

  Lemma subset_union_both : (P1 P2 Q1 Q2 : set),
    subset P1 Q1subset P2 Q2subset (union P1 P2) (union Q1 Q2).

  Lemma subset_union_lub : (P1 P2 Q : set),
    subset P1 Qsubset P2 Qsubset (union P1 P2) Q.

set equality

  Definition set_equal(P Q : set) : Prop :=
    (a : A), P a Q a.

  Lemma set_equal_refl : (P : set), set_equal P P.

  Lemma set_equal_symm : (P Q : set),
    set_equal Q Pset_equal P Q.

  Lemma set_equal_trans : (P1 P2 P3 : set),
    set_equal P1 P2set_equal P2 P3set_equal P1 P3.

  Lemma set_equal_subset_char : (P Q : set),
    set_equal P Q (subset P Q subset Q P).

  Lemma set_equal_subset : (P1 P2 : set)(Q1 Q2 : set),
    set_equal P1 P2
    set_equal Q1 Q2
    subset P1 Q1
      subset P2 Q2.

  Lemma union_comm : (P Q : set),
    set_equal (union P Q) (union Q P).

  Lemma set_equal_union : (P1 P2 Q1 Q2 : set),
    set_equal P1 Q1
    set_equal P2 Q2
      set_equal (union P1 P2) (union Q1 Q2).

  Lemma set_equal_intersection : (P1 P2 Q1 Q2 : set),
    set_equal P1 Q1
    set_equal P2 Q2
      set_equal (intersection P1 P2) (intersection Q1 Q2).

  Lemma set_equal_set_inverse : (P Q : set),
    set_equal P Qset_equal (set_inverse P) (set_inverse Q).

  Lemma set_equal_is_full : (P Q : set),
    set_equal P Q
    is_full_set P
      is_full_set Q.

  Lemma set_equal_union_subset_right : (P Q : set),
    subset Q Pset_equal (union P Q) P.

  Lemma subset_empty_set : (P : set), subset empty_set P.

  Lemma set_equal_union_empty_right : (P Q : set),
    set_equal Q empty_setset_equal (union P Q) P.

  Lemma set_equal_implies_subset : (P Q : set),
    set_equal P Qsubset P Q.

  Lemma set_equal_rw_r : (P1 P2 P3 : set),
    set_equal P2 P3set_equal P1 P3set_equal P1 P2.


  Lemma intersection_complement : (P : set)(a : A),
    not (intersection P (set_inverse P) a).

  Lemma set_inverse_intersection : (P Q : set)(a : A),
    union (set_inverse P) (set_inverse Q) a
      set_inverse (intersection P Q) a.

  Lemma double_set_inverse : (P : set)(a : A),
    P aset_inverse (set_inverse P) a.

full set

  Lemma full_set_full : is_full_set full_set.

  Lemma full_subset_full :
    (P : set), subset full_set Pis_full_set P.

End Sets.

Implicit Arguments is_full_set [A].
Implicit Arguments add [A].
Implicit Arguments subset [A].
Implicit Arguments union [A].
Implicit Arguments intersection [[A]].
Implicit Arguments set_inverse [[A]].
Implicit Arguments set_equal [A].

Definition sets_containing{A : Type}(a : A) : set (set A) :=
  fun(s : set A) ⇒ s a.