(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

Require Export Ensembles.
Require Export Constructive_sets.
Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Partial_Order.
Require Export Cpo.
Require Export Powerset.

Section Sets_as_an_algebra.
  Variable U : Type.

  Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
U:Type
forall X : Ensemble U, Union U (Empty_set U) X = X
  Proof.
U:Type
forall X : Ensemble U, Union U (Empty_set U) X = X
    auto 6 with sets.
  Qed.

  Theorem Empty_set_zero_right : forall X:Ensemble U, Union U X (Empty_set U) = X.
U:Type
forall X : Ensemble U, Union U X (Empty_set U) = X
  Proof.
U:Type
forall X : Ensemble U, Union U X (Empty_set U) = X
    auto 6 with sets.
  Qed.

  Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
U:Type
forall x : U, Add U (Empty_set U) x = Singleton U x
  Proof.
U:Type
forall x : U, Add U (Empty_set U) x = Singleton U x
    unfold Add at 1; auto using Empty_set_zero with sets.
  Qed.

  Lemma less_than_empty :
    forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
U:Type
forall X : Ensemble U,
Included U X (Empty_set U) -> X = Empty_set U
  Proof.
U:Type
forall X : Ensemble U,
Included U X (Empty_set U) -> X = Empty_set U
    auto with sets.
  Qed.

  Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
U:Type
forall A B : Ensemble U, Union U A B = Union U B A
  Proof.
U:Type
forall A B : Ensemble U, Union U A B = Union U B A
    auto with sets.
  Qed.

  Theorem Union_associative :
    forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
U:Type
forall A B C : Ensemble U,
Union U (Union U A B) C = Union U A (Union U B C)
  Proof.
U:Type
forall A B C : Ensemble U,
Union U (Union U A B) C = Union U A (Union U B C)
    auto 9 with sets.
  Qed.

  Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
U:Type
forall A : Ensemble U, Union U A A = A
  Proof.
U:Type
forall A : Ensemble U, Union U A A = A
    auto 7 with sets.
  Qed.

  Lemma Union_absorbs :
    forall A B:Ensemble U, Included U B A -> Union U A B = A.
U:Type
forall A B : Ensemble U,
Included U B A -> Union U A B = A
  Proof.
U:Type
forall A B : Ensemble U,
Included U B A -> Union U A B = A
    auto 7 with sets.
  Qed.

  Theorem Couple_as_union :
    forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
U:Type
forall x y : U,
Union U (Singleton U x) (Singleton U y) = Couple U x y
  Proof.
U:Type
forall x y : U,
Union U (Singleton U x) (Singleton U y) = Couple U x y
    intros x y; apply Extensionality_Ensembles; split; red.
U:Type
x, y:U
forall x0 : U,
In U (Union U (Singleton U x) (Singleton U y)) x0 ->
In U (Couple U x y) x0
U:Type
x, y:U
forall x0 : U,
In U (Couple U x y) x0 ->
In U (Union U (Singleton U x) (Singleton U y)) x0
    -
U:Type
x, y:U
forall x0 : U,
In U (Union U (Singleton U x) (Singleton U y)) x0 ->
In U (Couple U x y) x0 intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
    -
U:Type
x, y:U
forall x0 : U,
In U (Couple U x y) x0 ->
In U (Union U (Singleton U x) (Singleton U y)) x0 intros x0 H'; elim H'; auto with sets.
  Qed.

  Theorem Triple_as_union :
    forall x y z:U,
      Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
      Triple U x y z.
U:Type
forall x y z : U,
Union U (Union U (Singleton U x) (Singleton U y))
  (Singleton U z) = Triple U x y z
  Proof.
U:Type
forall x y z : U,
Union U (Union U (Singleton U x) (Singleton U y))
  (Singleton U z) = Triple U x y z
    intros x y z; apply Extensionality_Ensembles; split; red.
U:Type
x, y, z:U
forall x0 : U,
In U
  (Union U (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0 -> In U (Triple U x y z) x0
U:Type
x, y, z:U
forall x0 : U,
In U (Triple U x y z) x0 ->
In U
  (Union U (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0
    -
U:Type
x, y, z:U
forall x0 : U,
In U
  (Union U (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0 -> In U (Triple U x y z) x0 intros x0 H'; elim H'.
U:Type
x, y, z, x0:U
H':In U
  (Union U
     (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0
forall x1 : U,
In U (Union U (Singleton U x) (Singleton U y)) x1 ->
In U (Triple U x y z) x1
U:Type
x, y, z, x0:U
H':In U
  (Union U
     (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0
forall x1 : U,
In U (Singleton U z) x1 -> In U (Triple U x y z) x1
      +
U:Type
x, y, z, x0:U
H':In U
  (Union U
     (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0
forall x1 : U,
In U (Union U (Singleton U x) (Singleton U y)) x1 ->
In U (Triple U x y z) x1 intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
      +
U:Type
x, y, z, x0:U
H':In U
  (Union U
     (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0
forall x1 : U,
In U (Singleton U z) x1 -> In U (Triple U x y z) x1 intros x1 H'0; elim H'0; auto with sets.
    -
U:Type
x, y, z:U
forall x0 : U,
In U (Triple U x y z) x0 ->
In U
  (Union U (Union U (Singleton U x) (Singleton U y))
     (Singleton U z)) x0 intros x0 H'; elim H'; auto with sets.
  Qed.

  Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
U:Type
forall x y : U, Couple U x y = Triple U x x y
  Proof.
U:Type
forall x y : U, Couple U x y = Triple U x x y
    intros x y.
U:Type
x, y:U
Couple U x y = Triple U x x y
    rewrite <- (Couple_as_union x y).
U:Type
x, y:U
Union U (Singleton U x) (Singleton U y) =
Triple U x x y
    rewrite <- (Union_idempotent (Singleton U x)).
U:Type
x, y:U
Union U (Union U (Singleton U x) (Singleton U x))
  (Singleton U y) = Triple U x x y
    apply Triple_as_union.
  Qed.

  Theorem Triple_as_Couple_Singleton :
    forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
U:Type
forall x y z : U,
Triple U x y z =
Union U (Couple U x y) (Singleton U z)
  Proof.
U:Type
forall x y z : U,
Triple U x y z =
Union U (Couple U x y) (Singleton U z)
    intros x y z.
U:Type
x, y, z:U
Triple U x y z =
Union U (Couple U x y) (Singleton U z)
    rewrite <- (Triple_as_union x y z).
U:Type
x, y, z:U
Union U (Union U (Singleton U x) (Singleton U y))
  (Singleton U z) =
Union U (Couple U x y) (Singleton U z)
    rewrite <- (Couple_as_union x y); auto with sets.
  Qed.

  Theorem Intersection_commutative :
    forall A B:Ensemble U, Intersection U A B = Intersection U B A.
U:Type
forall A B : Ensemble U,
Intersection U A B = Intersection U B A
  Proof.
U:Type
forall A B : Ensemble U,
Intersection U A B = Intersection U B A
    intros A B.
U:Type
A, B:Ensemble U
Intersection U A B = Intersection U B A
    apply Extensionality_Ensembles.
U:Type
A, B:Ensemble U
Same_set U (Intersection U A B) (Intersection U B A)
    split; red; intros x H'; elim H'; auto with sets.
  Qed.

  Theorem Distributivity :
    forall A B C:Ensemble U,
      Intersection U A (Union U B C) =
      Union U (Intersection U A B) (Intersection U A C).
U:Type
forall A B C : Ensemble U,
Intersection U A (Union U B C) =
Union U (Intersection U A B) (Intersection U A C)
  Proof.
U:Type
forall A B C : Ensemble U,
Intersection U A (Union U B C) =
Union U (Intersection U A B) (Intersection U A C)
    intros A B C.
U:Type
A, B, C:Ensemble U
Intersection U A (Union U B C) =
Union U (Intersection U A B) (Intersection U A C)
    apply Extensionality_Ensembles.
U:Type
A, B, C:Ensemble U
Same_set U (Intersection U A (Union U B C))
  (Union U (Intersection U A B) (Intersection U A C))
    split; red; intros x H'.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U A (Union U B C)) x
In U
  (Union U (Intersection U A B) (Intersection U A C))
  x
U:Type
A, B, C:Ensemble U
x:U
H':In U
  (Union U (Intersection U A B)
     (Intersection U A C)) x
In U (Intersection U A (Union U B C)) x
    -
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U A (Union U B C)) x
In U
  (Union U (Intersection U A B) (Intersection U A C))
  x elim H'.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U A (Union U B C)) x
forall x0 : U,
In U A x0 ->
In U (Union U B C) x0 ->
In U
  (Union U (Intersection U A B) (Intersection U A C))
  x0
      intros x0 H'0 H'1; generalize H'0.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U A (Union U B C)) x
x0:U
H'0:In U A x0
H'1:In U (Union U B C) x0
In U A x0 ->
In U
  (Union U (Intersection U A B) (Intersection U A C))
  x0
      elim H'1; auto with sets.
    -
U:Type
A, B, C:Ensemble U
x:U
H':In U
  (Union U (Intersection U A B)
     (Intersection U A C)) x
In U (Intersection U A (Union U B C)) x elim H'; intros x0 H'0; elim H'0; auto with sets.
  Qed.

  Lemma Distributivity_l
       : forall (A B C : Ensemble U),
         Intersection U (Union U A B) C =
         Union U (Intersection U A C) (Intersection U B C).
U:Type
forall A B C : Ensemble U,
Intersection U (Union U A B) C =
Union U (Intersection U A C) (Intersection U B C)
  Proof.
U:Type
forall A B C : Ensemble U,
Intersection U (Union U A B) C =
Union U (Intersection U A C) (Intersection U B C)
     intros  A B C.
U:Type
A, B, C:Ensemble U
Intersection U (Union U A B) C =
Union U (Intersection U A C) (Intersection U B C)
     rewrite Intersection_commutative.
U:Type
A, B, C:Ensemble U
Intersection U C (Union U A B) =
Union U (Intersection U A C) (Intersection U B C)
     rewrite Distributivity.
U:Type
A, B, C:Ensemble U
Union U (Intersection U C A) (Intersection U C B) =
Union U (Intersection U A C) (Intersection U B C)
     f_equal; apply Intersection_commutative.
  Qed.

  Theorem Distributivity' :
    forall A B C:Ensemble U,
      Union U A (Intersection U B C) =
      Intersection U (Union U A B) (Union U A C).
U:Type
forall A B C : Ensemble U,
Union U A (Intersection U B C) =
Intersection U (Union U A B) (Union U A C)
  Proof.
U:Type
forall A B C : Ensemble U,
Union U A (Intersection U B C) =
Intersection U (Union U A B) (Union U A C)
    intros A B C.
U:Type
A, B, C:Ensemble U
Union U A (Intersection U B C) =
Intersection U (Union U A B) (Union U A C)
    apply Extensionality_Ensembles.
U:Type
A, B, C:Ensemble U
Same_set U (Union U A (Intersection U B C))
  (Intersection U (Union U A B) (Union U A C))
    split; red; intros x H'.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Union U A (Intersection U B C)) x
In U (Intersection U (Union U A B) (Union U A C)) x
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U (Union U A B) (Union U A C))
  x
In U (Union U A (Intersection U B C)) x
    -
U:Type
A, B, C:Ensemble U
x:U
H':In U (Union U A (Intersection U B C)) x
In U (Intersection U (Union U A B) (Union U A C)) x elim H'; auto with sets.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Union U A (Intersection U B C)) x
forall x0 : U,
In U (Intersection U B C) x0 ->
In U (Intersection U (Union U A B) (Union U A C)) x0
      intros x0 H'0; elim H'0; auto with sets.
    -
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U (Union U A B) (Union U A C))
  x
In U (Union U A (Intersection U B C)) x elim H'.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U (Union U A B) (Union U A C))
  x
forall x0 : U,
In U (Union U A B) x0 ->
In U (Union U A C) x0 ->
In U (Union U A (Intersection U B C)) x0
      intros x0 H'0; elim H'0; auto with sets.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U (Union U A B) (Union U A C))
  x
x0:U
H'0:In U (Union U A B) x0
forall x1 : U,
In U B x1 ->
In U (Union U A C) x1 ->
In U (Union U A (Intersection U B C)) x1
      intros x1 H'1 H'2; try exact H'2.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U (Union U A B) (Union U A C))
  x
x0:U
H'0:In U (Union U A B) x0
x1:U
H'1:In U B x1
H'2:In U (Union U A C) x1
In U (Union U A (Intersection U B C)) x1
      generalize H'1.
U:Type
A, B, C:Ensemble U
x:U
H':In U (Intersection U (Union U A B) (Union U A C))
  x
x0:U
H'0:In U (Union U A B) x0
x1:U
H'1:In U B x1
H'2:In U (Union U A C) x1
In U B x1 -> In U (Union U A (Intersection U B C)) x1
      elim H'2; auto with sets.
  Qed.

  Theorem Union_add :
    forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
U:Type
forall (A B : Ensemble U) (x : U),
Add U (Union U A B) x = Union U A (Add U B x)
  Proof.
U:Type
forall (A B : Ensemble U) (x : U),
Add U (Union U A B) x = Union U A (Add U B x)
    unfold Add; auto using Union_associative with sets.
  Qed.

  Theorem Non_disjoint_union :
    forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Add U X x = X
  Proof.
U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Add U X x = X
    intros X x H'; unfold Add.
U:Type
X:Ensemble U
x:U
H':In U X x
Union U X (Singleton U x) = X
    apply Extensionality_Ensembles; red.
U:Type
X:Ensemble U
x:U
H':In U X x
Included U (Union U X (Singleton U x)) X /\
Included U X (Union U X (Singleton U x))
    split; red; auto with sets.
U:Type
X:Ensemble U
x:U
H':In U X x
forall x0 : U,
In U (Union U X (Singleton U x)) x0 -> In U X x0
    intros x0 H'0; elim H'0; auto with sets.
U:Type
X:Ensemble U
x:U
H':In U X x
x0:U
H'0:In U (Union U X (Singleton U x)) x0
forall x1 : U, In U (Singleton U x) x1 -> In U X x1
    intros t H'1; elim H'1; auto with sets.
  Qed.

  Theorem Non_disjoint_union' :
    forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
U:Type
forall (X : Ensemble U) (x : U),
~ In U X x -> Subtract U X x = X
  Proof.
U:Type
forall (X : Ensemble U) (x : U),
~ In U X x -> Subtract U X x = X
    intros X x H'; unfold Subtract.
U:Type
X:Ensemble U
x:U
H':~ In U X x
Setminus U X (Singleton U x) = X
    apply Extensionality_Ensembles.
U:Type
X:Ensemble U
x:U
H':~ In U X x
Same_set U (Setminus U X (Singleton U x)) X
    split; red; auto with sets.
U:Type
X:Ensemble U
x:U
H':~ In U X x
forall x0 : U,
In U (Setminus U X (Singleton U x)) x0 -> In U X x0
U:Type
X:Ensemble U
x:U
H':~ In U X x
forall x0 : U,
In U X x0 -> In U (Setminus U X (Singleton U x)) x0
    -
U:Type
X:Ensemble U
x:U
H':~ In U X x
forall x0 : U,
In U (Setminus U X (Singleton U x)) x0 -> In U X x0 intros x0 H'0; elim H'0; auto with sets.
    -
U:Type
X:Ensemble U
x:U
H':~ In U X x
forall x0 : U,
In U X x0 -> In U (Setminus U X (Singleton U x)) x0 intros x0 H'0; apply Setminus_intro; auto with sets.
U:Type
X:Ensemble U
x:U
H':~ In U X x
x0:U
H'0:In U X x0
~ In U (Singleton U x) x0
      red; intro H'1; elim H'1.
U:Type
X:Ensemble U
x:U
H':~ In U X x
x0:U
H'0:In U X x0
H'1:In U (Singleton U x) x0
False
      lapply (Singleton_inv U x x0); auto with sets.
U:Type
X:Ensemble U
x:U
H':~ In U X x
x0:U
H'0:In U X x0
H'1:In U (Singleton U x) x0
x = x0 -> False
      intro H'4; apply H'; rewrite H'4; auto with sets.
  Qed.

  Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
U:Type
forall x y : U,
In U (Add U (Empty_set U) x) y -> x = y
  Proof.
U:Type
forall x y : U,
In U (Add U (Empty_set U) x) y -> x = y
    intro x; rewrite (Empty_set_zero' x); auto with sets.
  Qed.

  Lemma incl_add :
    forall (A B:Ensemble U) (x:U),
      Included U A B -> Included U (Add U A x) (Add U B x).
U:Type
forall (A B : Ensemble U) (x : U),
Included U A B -> Included U (Add U A x) (Add U B x)
  Proof.
U:Type
forall (A B : Ensemble U) (x : U),
Included U A B -> Included U (Add U A x) (Add U B x)
    intros A B x H'; red; auto with sets.
U:Type
A, B:Ensemble U
x:U
H':Included U A B
forall x0 : U,
In U (Add U A x) x0 -> In U (Add U B x) x0
    intros x0 H'0.
U:Type
A, B:Ensemble U
x:U
H':Included U A B
x0:U
H'0:In U (Add U A x) x0
In U (Add U B x) x0
    lapply (Add_inv U A x x0); auto with sets.
U:Type
A, B:Ensemble U
x:U
H':Included U A B
x0:U
H'0:In U (Add U A x) x0
In U A x0 \/ x = x0 -> In U (Add U B x) x0
    intro H'1; elim H'1;
      [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
      auto with sets.
  Qed.

  Lemma incl_add_x :
    forall (A B:Ensemble U) (x:U),
      ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
U:Type
forall (A B : Ensemble U) (x : U),
~ In U A x ->
Included U (Add U A x) (Add U B x) -> Included U A B
  Proof.
U:Type
forall (A B : Ensemble U) (x : U),
~ In U A x ->
Included U (Add U A x) (Add U B x) -> Included U A B
    unfold Included.
U:Type
forall (A B : Ensemble U) (x : U),
~ In U A x ->
(forall x0 : U,
 In U (Add U A x) x0 -> In U (Add U B x) x0) ->
forall x0 : U, In U A x0 -> In U B x0
    intros A B x H' H'0 x0 H'1.
U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:forall x1 : U, In U (Add U A x) x1 -> In U (Add U B x) x1
x0:U
H'1:In U A x0
In U B x0
    lapply (H'0 x0); auto with sets.
U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:forall x1 : U, In U (Add U A x) x1 -> In U (Add U B x) x1
x0:U
H'1:In U A x0
In U (Add U B x) x0 -> In U B x0
    intro H'2; lapply (Add_inv U B x x0); auto with sets.
U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:forall x1 : U, In U (Add U A x) x1 -> In U (Add U B x) x1
x0:U
H'1:In U A x0
H'2:In U (Add U B x) x0
In U B x0 \/ x = x0 -> In U B x0
    intro H'3; elim H'3;
      [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:forall x1 : U, In U (Add U A x) x1 -> In U (Add U B x) x1
x0:U
H'1:In U A x0
H'2:In U (Add U B x) x0
H'4:x = x0
In U B x0
    absurd (In U A x0); auto with sets.
U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:forall x1 : U, In U (Add U A x) x1 -> In U (Add U B x) x1
x0:U
H'1:In U A x0
H'2:In U (Add U B x) x0
H'4:x = x0
~ In U A x0
    rewrite <- H'4; auto with sets.
  Qed.

  Lemma Add_commutative :
    forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
U:Type
forall (A : Ensemble U) (x y : U),
Add U (Add U A x) y = Add U (Add U A y) x
  Proof.
U:Type
forall (A : Ensemble U) (x y : U),
Add U (Add U A x) y = Add U (Add U A y) x
    intros A x y.
U:Type
A:Ensemble U
x, y:U
Add U (Add U A x) y = Add U (Add U A y) x
    unfold Add.
U:Type
A:Ensemble U
x, y:U
Union U (Union U A (Singleton U x)) (Singleton U y) =
Union U (Union U A (Singleton U y)) (Singleton U x)
    rewrite (Union_associative A (Singleton U x) (Singleton U y)).
U:Type
A:Ensemble U
x, y:U
Union U A (Union U (Singleton U x) (Singleton U y)) =
Union U (Union U A (Singleton U y)) (Singleton U x)
    rewrite (Union_commutative (Singleton U x) (Singleton U y)).
U:Type
A:Ensemble U
x, y:U
Union U A (Union U (Singleton U y) (Singleton U x)) =
Union U (Union U A (Singleton U y)) (Singleton U x)
    rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
      auto with sets.
  Qed.

  Lemma Add_commutative' :
    forall (A:Ensemble U) (x y z:U),
      Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
U:Type
forall (A : Ensemble U) (x y z : U),
Add U (Add U (Add U A x) y) z =
Add U (Add U (Add U A z) x) y
  Proof.
U:Type
forall (A : Ensemble U) (x y z : U),
Add U (Add U (Add U A x) y) z =
Add U (Add U (Add U A z) x) y
    intros A x y z.
U:Type
A:Ensemble U
x, y, z:U
Add U (Add U (Add U A x) y) z =
Add U (Add U (Add U A z) x) y
    rewrite (Add_commutative (Add U A x) y z).
U:Type
A:Ensemble U
x, y, z:U
Add U (Add U (Add U A x) z) y =
Add U (Add U (Add U A z) x) y
    rewrite (Add_commutative A x z); auto with sets.
  Qed.

  Lemma Add_distributes :
    forall (A B:Ensemble U) (x y:U),
      Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
U:Type
forall (A B : Ensemble U) (x y : U),
Included U B A ->
Add U (Add U A x) y = Union U (Add U A x) (Add U B y)
  Proof.
U:Type
forall (A B : Ensemble U) (x y : U),
Included U B A ->
Add U (Add U A x) y = Union U (Add U A x) (Add U B y)
    intros A B x y H'; try assumption.
U:Type
A, B:Ensemble U
x, y:U
H':Included U B A
Add U (Add U A x) y = Union U (Add U A x) (Add U B y)
    rewrite <- (Union_add (Add U A x) B y).
U:Type
A, B:Ensemble U
x, y:U
H':Included U B A
Add U (Add U A x) y = Add U (Union U (Add U A x) B) y
    unfold Add at 4.
U:Type
A, B:Ensemble U
x, y:U
H':Included U B A
Add U (Add U A x) y =
Add U (Union U (Union U A (Singleton U x)) B) y
    rewrite (Union_commutative A (Singleton U x)).
U:Type
A, B:Ensemble U
x, y:U
H':Included U B A
Add U (Add U A x) y =
Add U (Union U (Union U (Singleton U x) A) B) y
    rewrite Union_associative.
U:Type
A, B:Ensemble U
x, y:U
H':Included U B A
Add U (Add U A x) y =
Add U (Union U (Singleton U x) (Union U A B)) y
    rewrite (Union_absorbs A B H').
U:Type
A, B:Ensemble U
x, y:U
H':Included U B A
Add U (Add U A x) y =
Add U (Union U (Singleton U x) A) y
    rewrite (Union_commutative (Singleton U x) A).
U:Type
A, B:Ensemble U
x, y:U
H':Included U B A
Add U (Add U A x) y =
Add U (Union U A (Singleton U x)) y
    auto with sets.
  Qed.

  Lemma setcover_intro :
    forall (U:Type) (A x y:Ensemble U),
      Strict_Included U x y ->
      ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->
      covers (Ensemble U) (Power_set_PO U A) y x.
U:Type
forall (U0 : Type) (A x y : Ensemble U0),
Strict_Included U0 x y ->
~
(exists z : Ensemble U0,
   Strict_Included U0 x z /\ Strict_Included U0 z y) ->
covers (Ensemble U0) (Power_set_PO U0 A) y x
  Proof.
U:Type
forall (U0 : Type) (A x y : Ensemble U0),
Strict_Included U0 x y ->
~
(exists z : Ensemble U0,
   Strict_Included U0 x z /\ Strict_Included U0 z y) ->
covers (Ensemble U0) (Power_set_PO U0 A) y x
    intros; apply Definition_of_covers; auto with sets.
  Qed.

  Lemma Disjoint_Intersection:
    forall A s1 s2, Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A.
U:Type
forall (A : Type) (s1 s2 : Ensemble A),
Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A
  Proof.
U:Type
forall (A : Type) (s1 s2 : Ensemble A),
Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A
    intros.
U, A:Type
s1, s2:Ensemble A
H:Disjoint A s1 s2
Intersection A s1 s2 = Empty_set A apply Extensionality_Ensembles.
U, A:Type
s1, s2:Ensemble A
H:Disjoint A s1 s2
Same_set A (Intersection A s1 s2) (Empty_set A) split.
U, A:Type
s1, s2:Ensemble A
H:Disjoint A s1 s2
Included A (Intersection A s1 s2) (Empty_set A)
U, A:Type
s1, s2:Ensemble A
H:Disjoint A s1 s2
Included A (Empty_set A) (Intersection A s1 s2)
    *
U, A:Type
s1, s2:Ensemble A
H:Disjoint A s1 s2
Included A (Intersection A s1 s2) (Empty_set A) destruct H.
U, A:Type
s1, s2:Ensemble A
H:forall x : A, ~ In A (Intersection A s1 s2) x
Included A (Intersection A s1 s2) (Empty_set A)
      intros x H1.
U, A:Type
s1, s2:Ensemble A
H:forall x0 : A, ~ In A (Intersection A s1 s2) x0
x:A
H1:In A (Intersection A s1 s2) x
In A (Empty_set A) x unfold In in *.
U, A:Type
s1, s2:Ensemble A
H:forall x0 : A, ~ Intersection A s1 s2 x0
x:A
H1:Intersection A s1 s2 x
Empty_set A x exfalso.
U, A:Type
s1, s2:Ensemble A
H:forall x0 : A, ~ Intersection A s1 s2 x0
x:A
H1:Intersection A s1 s2 x
False intuition.
U, A:Type
s1, s2:Ensemble A
H:forall x0 : A, Intersection A s1 s2 x0 -> False
x:A
H1:Intersection A s1 s2 x
False apply (H _ H1).
    *
U, A:Type
s1, s2:Ensemble A
H:Disjoint A s1 s2
Included A (Empty_set A) (Intersection A s1 s2) intuition.
  Qed.

  Lemma Intersection_Empty_set_l:
    forall A s, Intersection A (Empty_set A) s = Empty_set A.
U:Type
forall (A : Type) (s : Ensemble A),
Intersection A (Empty_set A) s = Empty_set A
  Proof.
U:Type
forall (A : Type) (s : Ensemble A),
Intersection A (Empty_set A) s = Empty_set A
    intros.
U, A:Type
s:Ensemble A
Intersection A (Empty_set A) s = Empty_set A auto with sets.
  Qed.

  Lemma Intersection_Empty_set_r:
    forall A s, Intersection A s (Empty_set A) = Empty_set A.
U:Type
forall (A : Type) (s : Ensemble A),
Intersection A s (Empty_set A) = Empty_set A
  Proof.
U:Type
forall (A : Type) (s : Ensemble A),
Intersection A s (Empty_set A) = Empty_set A
    intros.
U, A:Type
s:Ensemble A
Intersection A s (Empty_set A) = Empty_set A auto with sets.
  Qed.

  Lemma Seminus_Empty_set_l:
    forall A s, Setminus A (Empty_set A) s = Empty_set A.
U:Type
forall (A : Type) (s : Ensemble A),
Setminus A (Empty_set A) s = Empty_set A
  Proof.
U:Type
forall (A : Type) (s : Ensemble A),
Setminus A (Empty_set A) s = Empty_set A
    intros.
U, A:Type
s:Ensemble A
Setminus A (Empty_set A) s = Empty_set A apply Extensionality_Ensembles.
U, A:Type
s:Ensemble A
Same_set A (Setminus A (Empty_set A) s) (Empty_set A) split.
U, A:Type
s:Ensemble A
Included A (Setminus A (Empty_set A) s) (Empty_set A)
U, A:Type
s:Ensemble A
Included A (Empty_set A) (Setminus A (Empty_set A) s)
    *
U, A:Type
s:Ensemble A
Included A (Setminus A (Empty_set A) s) (Empty_set A) intros x H1.
U, A:Type
s:Ensemble A
x:A
H1:In A (Setminus A (Empty_set A) s) x
In A (Empty_set A) x destruct H1.
U, A:Type
s:Ensemble A
x:A
H:In A (Empty_set A) x
H0:~ In A s x
In A (Empty_set A) x unfold In in *.
U, A:Type
s:Ensemble A
x:A
H:Empty_set A x
H0:~ s x
Empty_set A x assumption.
    *
U, A:Type
s:Ensemble A
Included A (Empty_set A) (Setminus A (Empty_set A) s) intuition.
  Qed.

  Lemma Seminus_Empty_set_r:
    forall A s, Setminus A s (Empty_set A) = s.
U:Type
forall (A : Type) (s : Ensemble A),
Setminus A s (Empty_set A) = s
  Proof.
U:Type
forall (A : Type) (s : Ensemble A),
Setminus A s (Empty_set A) = s
    intros.
U, A:Type
s:Ensemble A
Setminus A s (Empty_set A) = s apply Extensionality_Ensembles.
U, A:Type
s:Ensemble A
Same_set A (Setminus A s (Empty_set A)) s split.
U, A:Type
s:Ensemble A
Included A (Setminus A s (Empty_set A)) s
U, A:Type
s:Ensemble A
Included A s (Setminus A s (Empty_set A))
    *
U, A:Type
s:Ensemble A
Included A (Setminus A s (Empty_set A)) s intros x H1.
U, A:Type
s:Ensemble A
x:A
H1:In A (Setminus A s (Empty_set A)) x
In A s x destruct H1.
U, A:Type
s:Ensemble A
x:A
H:In A s x
H0:~ In A (Empty_set A) x
In A s x unfold In in *.
U, A:Type
s:Ensemble A
x:A
H:s x
H0:~ Empty_set A x
s x assumption.
    *
U, A:Type
s:Ensemble A
Included A s (Setminus A s (Empty_set A)) intuition.
  Qed.

  Lemma Setminus_Union_l:
    forall A s1 s2 s3,
    Setminus A (Union A s1 s2) s3 = Union A (Setminus A s1 s3)  (Setminus A s2 s3).
U:Type
forall (A : Type) (s1 s2 s3 : Ensemble A),
Setminus A (Union A s1 s2) s3 =
Union A (Setminus A s1 s3) (Setminus A s2 s3)
  Proof.
U:Type
forall (A : Type) (s1 s2 s3 : Ensemble A),
Setminus A (Union A s1 s2) s3 =
Union A (Setminus A s1 s3) (Setminus A s2 s3)
    intros.
U, A:Type
s1, s2, s3:Ensemble A
Setminus A (Union A s1 s2) s3 =
Union A (Setminus A s1 s3) (Setminus A s2 s3) apply Extensionality_Ensembles.
U, A:Type
s1, s2, s3:Ensemble A
Same_set A (Setminus A (Union A s1 s2) s3)
  (Union A (Setminus A s1 s3) (Setminus A s2 s3)) split.
U, A:Type
s1, s2, s3:Ensemble A
Included A (Setminus A (Union A s1 s2) s3)
  (Union A (Setminus A s1 s3) (Setminus A s2 s3))
U, A:Type
s1, s2, s3:Ensemble A
Included A
  (Union A (Setminus A s1 s3) (Setminus A s2 s3))
  (Setminus A (Union A s1 s2) s3)
    *
U, A:Type
s1, s2, s3:Ensemble A
Included A (Setminus A (Union A s1 s2) s3)
  (Union A (Setminus A s1 s3) (Setminus A s2 s3)) intros x H.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A (Union A s1 s2) s3) x
In A (Union A (Setminus A s1 s3) (Setminus A s2 s3)) x inversion H.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A (Union A s1 s2) s3) x
H0:In A (Union A s1 s2) x
H1:~ In A s3 x
In A (Union A (Setminus A s1 s3) (Setminus A s2 s3)) x inversion H0; intuition.
    *
U, A:Type
s1, s2, s3:Ensemble A
Included A
  (Union A (Setminus A s1 s3) (Setminus A s2 s3))
  (Setminus A (Union A s1 s2) s3) intros x H.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A
  (Union A (Setminus A s1 s3) (Setminus A s2 s3))
  x
In A (Setminus A (Union A s1 s2) s3) x constructor; inversion H; inversion H0; intuition.
  Qed.

  Lemma Setminus_Union_r:
    forall A s1 s2 s3,
    Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3.
U:Type
forall (A : Type) (s1 s2 s3 : Ensemble A),
Setminus A s1 (Union A s2 s3) =
Setminus A (Setminus A s1 s2) s3
  Proof.
U:Type
forall (A : Type) (s1 s2 s3 : Ensemble A),
Setminus A s1 (Union A s2 s3) =
Setminus A (Setminus A s1 s2) s3
    intros.
U, A:Type
s1, s2, s3:Ensemble A
Setminus A s1 (Union A s2 s3) =
Setminus A (Setminus A s1 s2) s3 apply Extensionality_Ensembles.
U, A:Type
s1, s2, s3:Ensemble A
Same_set A (Setminus A s1 (Union A s2 s3))
  (Setminus A (Setminus A s1 s2) s3) split.
U, A:Type
s1, s2, s3:Ensemble A
Included A (Setminus A s1 (Union A s2 s3))
  (Setminus A (Setminus A s1 s2) s3)
U, A:Type
s1, s2, s3:Ensemble A
Included A (Setminus A (Setminus A s1 s2) s3)
  (Setminus A s1 (Union A s2 s3))
    *
U, A:Type
s1, s2, s3:Ensemble A
Included A (Setminus A s1 (Union A s2 s3))
  (Setminus A (Setminus A s1 s2) s3) intros x H.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A s1 (Union A s2 s3)) x
In A (Setminus A (Setminus A s1 s2) s3) x inversion H.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A s1 (Union A s2 s3)) x
H0:In A s1 x
H1:~ In A (Union A s2 s3) x
In A (Setminus A (Setminus A s1 s2) s3) x constructor.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A s1 (Union A s2 s3)) x
H0:In A s1 x
H1:~ In A (Union A s2 s3) x
In A (Setminus A s1 s2) x
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A s1 (Union A s2 s3)) x
H0:In A s1 x
H1:~ In A (Union A s2 s3) x
~ In A s3 x
      --
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A s1 (Union A s2 s3)) x
H0:In A s1 x
H1:~ In A (Union A s2 s3) x
In A (Setminus A s1 s2) x intuition.
      --
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A s1 (Union A s2 s3)) x
H0:In A s1 x
H1:~ In A (Union A s2 s3) x
~ In A s3 x contradict H1.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A s1 (Union A s2 s3)) x
H0:In A s1 x
H1:In A s3 x
In A (Union A s2 s3) x intuition.
    *
U, A:Type
s1, s2, s3:Ensemble A
Included A (Setminus A (Setminus A s1 s2) s3)
  (Setminus A s1 (Union A s2 s3)) intros x H.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A (Setminus A s1 s2) s3) x
In A (Setminus A s1 (Union A s2 s3)) x inversion H.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A (Setminus A s1 s2) s3) x
H0:In A (Setminus A s1 s2) x
H1:~ In A s3 x
In A (Setminus A s1 (Union A s2 s3)) x inversion H0.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A (Setminus A s1 s2) s3) x
H0:In A (Setminus A s1 s2) x
H1:~ In A s3 x
H2:In A s1 x
H3:~ In A s2 x
In A (Setminus A s1 (Union A s2 s3)) x constructor; intuition.
U, A:Type
s1, s2, s3:Ensemble A
x:A
H:In A (Setminus A (Setminus A s1 s2) s3) x
H0:In A (Setminus A s1 s2) x
H1:In A s3 x -> False
H2:In A s1 x
H3:In A s2 x -> False
H4:In A (Union A s2 s3) x
False inversion H4; intuition.
  Qed.

 Lemma Setminus_Disjoint_noop:
    forall A s1 s2,
    Intersection A s1 s2 = Empty_set A -> Setminus A s1 s2 = s1.
U:Type
forall (A : Type) (s1 s2 : Ensemble A),
Intersection A s1 s2 = Empty_set A ->
Setminus A s1 s2 = s1
  Proof.
U:Type
forall (A : Type) (s1 s2 : Ensemble A),
Intersection A s1 s2 = Empty_set A ->
Setminus A s1 s2 = s1
    intros.
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
Setminus A s1 s2 = s1 apply Extensionality_Ensembles.
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
Same_set A (Setminus A s1 s2) s1 split.
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
Included A (Setminus A s1 s2) s1
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
Included A s1 (Setminus A s1 s2)
    *
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
Included A (Setminus A s1 s2) s1 intros x H1.
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
x:A
H1:In A (Setminus A s1 s2) x
In A s1 x inversion_clear H1.
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
x:A
H0:In A s1 x
H2:~ In A s2 x
In A s1 x intuition.
    *
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
Included A s1 (Setminus A s1 s2) intros x H1.
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
x:A
H1:In A s1 x
In A (Setminus A s1 s2) x constructor; intuition.
U, A:Type
s1, s2:Ensemble A
H:Intersection A s1 s2 = Empty_set A
x:A
H1:In A s1 x
H0:In A s2 x
False contradict H.
U, A:Type
s1, s2:Ensemble A
x:A
H1:In A s1 x
H0:In A s2 x
Intersection A s1 s2 <> Empty_set A
      apply Inhabited_not_empty.
U, A:Type
s1, s2:Ensemble A
x:A
H1:In A s1 x
H0:In A s2 x
Inhabited A (Intersection A s1 s2)
      exists x.
U, A:Type
s1, s2:Ensemble A
x:A
H1:In A s1 x
H0:In A s2 x
In A (Intersection A s1 s2) x intuition.
  Qed.

  Lemma Setminus_Included_empty:
    forall A s1 s2,
    Included A s1 s2 -> Setminus A s1 s2 = Empty_set A.
U:Type
forall (A : Type) (s1 s2 : Ensemble A),
Included A s1 s2 -> Setminus A s1 s2 = Empty_set A
  Proof.
U:Type
forall (A : Type) (s1 s2 : Ensemble A),
Included A s1 s2 -> Setminus A s1 s2 = Empty_set A
    intros.
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
Setminus A s1 s2 = Empty_set A apply Extensionality_Ensembles.
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
Same_set A (Setminus A s1 s2) (Empty_set A) split.
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
Included A (Setminus A s1 s2) (Empty_set A)
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
Included A (Empty_set A) (Setminus A s1 s2)
      *
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
Included A (Setminus A s1 s2) (Empty_set A) intros x H1.
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
x:A
H1:In A (Setminus A s1 s2) x
In A (Empty_set A) x inversion_clear H1.
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
x:A
H0:In A s1 x
H2:~ In A s2 x
In A (Empty_set A) x contradiction H2.
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
x:A
H0:In A s1 x
H2:~ In A s2 x
In A s2 x intuition.
      *
U, A:Type
s1, s2:Ensemble A
H:Included A s1 s2
Included A (Empty_set A) (Setminus A s1 s2) intuition.
  Qed.

End Sets_as_an_algebra.

Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
  singlx incl_add: sets.