Library Coq.Sets.Classical_sets

Require Export Ensembles.
Require Export Constructive_sets.
Require Export Classical.

Section Ensembles_classical.
  Variable U : Type.

  Lemma not_included_empty_Inhabited :
    forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.

  Lemma not_empty_Inhabited :
    forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.

  Lemma Inhabited_Setminus :
    forall X Y:Ensemble U,
      Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).

  Lemma Strict_super_set_contains_new_element :
    forall X Y:Ensemble U,
      Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).

  Lemma Subtract_intro :
    forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
  #[local]
  Hint Resolve Subtract_intro : sets.

  Lemma Subtract_inv :
    forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.

  Lemma Included_Strict_Included :
    forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.

  Lemma Strict_Included_inv :
    forall X Y:Ensemble U,
      Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).

  Lemma not_SIncl_empty :
    forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).

  Lemma Complement_Complement :
    forall A:Ensemble U, Complement U (Complement U A) = A.

End Ensembles_classical.

 #[global]
 Hint Resolve Strict_super_set_contains_new_element Subtract_intro
  not_SIncl_empty: sets.