Library Coq.Sets.Constructive_sets

Require Export Ensembles.

Section Ensembles_facts.
  Variable U : Type.

  Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.

  Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.

  Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.

  Lemma Add_intro1 :
    forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.

  Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.

  Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).

  Lemma Inhabited_not_empty :
    forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.

  Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.

  Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.

  Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.

  Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.

  Lemma Union_inv :
    forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.

  Lemma Add_inv :
    forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.

  Lemma Intersection_inv :
    forall (B C:Ensemble U) (x:U),
      In U (Intersection U B C) x -> In U B x /\ In U C x.

  Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.

  Lemma Setminus_intro :
    forall (A B:Ensemble U) (x:U),
      In U A x -> ~ In U B x -> In U (Setminus U A B) x.

  Lemma Strict_Included_intro :
    forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.

  Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.

End Ensembles_facts.

Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
  Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
  Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
  not_Empty_Add Inhabited_add Included_Empty: sets.