Powerset_Classical

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   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.
Require Export Powerset_facts.
Require Export Classical.
Require Export Classical_sets.

Section Sets_as_an_algebra.

  Variable U : Type.

  Lemma sincl_add_x :
    forall (A B:Ensemble U) (x:U),
      ~ In U A x ->
      Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.U:Type
forall (A B : Ensemble U) (x : U),
~ In U A x ->
Strict_Included U (Add U A x) (Add U B x) ->
Strict_Included U A B
  Proof.U:Type
forall (A B : Ensemble U) (x : U),
~ In U A x ->
Strict_Included U (Add U A x) (Add U B x) ->
Strict_Included U A B
    intros A B x H' H'0; red.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:Strict_Included U (Add U A x) (Add U B x)
Included U A B /\ A <> B
    lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:Strict_Included U (Add U A x) (Add U B x)
Included U (Add U A x) (Add U B x) /\
Inhabited U (Setminus U (Add U B x) (Add U A x)) ->
Included U A B /\ A <> B
    clear H'0; intro H'0; split.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:Included U (Add U A x) (Add U B x) /\
Inhabited U (Setminus U (Add U B x) (Add U A x))
Included U A B
U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:Included U (Add U A x) (Add U B x) /\
Inhabited U (Setminus U (Add U B x) (Add U A x))
A <> B
    apply incl_add_x with (x := x); tauto.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'0:Included U (Add U A x) (Add U B x) /\
Inhabited U (Setminus U (Add U B x) (Add U A x))
A <> B
    elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'1:Included U (Add U A x) (Add U B x)
forall x0 : U,
In U (Setminus U (Add U B x) (Add U A x)) x0 -> A <> B
    intros x0 H'0.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'1:Included U (Add U A x) (Add U B x)
x0:U
H'0:In U (Setminus U (Add U B x) (Add U A x)) x0
A <> B
    red; intro H'2.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'1:Included U (Add U A x) (Add U B x)
x0:U
H'0:In U (Setminus U (Add U B x) (Add U A x)) x0
H'2:A = B
False
    elim H'0; clear H'0.U:Type
A, B:Ensemble U
x:U
H':~ In U A x
H'1:Included U (Add U A x) (Add U B x)
x0:U
H'2:A = B
In U (Add U B x) x0 -> ~ In U (Add U A x) x0 -> False
    rewrite <- H'2; auto with sets.
  Qed.

  Lemma incl_soustr_in :
    forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Included U (Subtract U X x) X
  Proof.U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Included U (Subtract U X x) X
    intros X x H'; red.U:Type
X:Ensemble U
x:U
H':In U X x
forall x0 : U, In U (Subtract U X x) x0 -> In U X x0
    intros x0 H'0; elim H'0; auto with sets.
  Qed.

  Lemma incl_soustr :
    forall (X Y:Ensemble U) (x:U),
      Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).U:Type
forall (X Y : Ensemble U) (x : U),
Included U X Y ->
Included U (Subtract U X x) (Subtract U Y x)
  Proof.U:Type
forall (X Y : Ensemble U) (x : U),
Included U X Y ->
Included U (Subtract U X x) (Subtract U Y x)
    intros X Y x H'; red.U:Type
X, Y:Ensemble U
x:U
H':Included U X Y
forall x0 : U,
In U (Subtract U X x) x0 -> In U (Subtract U Y x) x0
    intros x0 H'0; elim H'0.U:Type
X, Y:Ensemble U
x:U
H':Included U X Y
x0:U
H'0:In U (Subtract U X x) x0
In U X x0 ->
~ In U (Singleton U x) x0 -> In U (Subtract U Y x) x0
    intros H'1 H'2.U:Type
X, Y:Ensemble U
x:U
H':Included U X Y
x0:U
H'0:In U (Subtract U X x) x0
H'1:In U X x0
H'2:~ In U (Singleton U x) x0
In U (Subtract U Y x) x0
    apply Subtract_intro; auto with sets.
  Qed.

  Lemma incl_soustr_add_l :
    forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.U:Type
forall (X : Ensemble U) (x : U),
Included U (Subtract U (Add U X x) x) X
  Proof.U:Type
forall (X : Ensemble U) (x : U),
Included U (Subtract U (Add U X x) x) X
    intros X x; red.U:Type
X:Ensemble U
x:U
forall x0 : U,
In U (Subtract U (Add U X x) x) x0 -> In U X x0
    intros x0 H'; elim H'; auto with sets.U:Type
X:Ensemble U
x, x0:U
H':In U (Subtract U (Add U X x) x) x0
In U (Add U X x) x0 ->
~ In U (Singleton U x) x0 -> In U X x0
    intro H'0; elim H'0; auto with sets.U:Type
X:Ensemble U
x, x0:U
H':In U (Subtract U (Add U X x) x) x0
H'0:In U (Add U X x) x0
forall x1 : U,
In U (Singleton U x) x1 ->
~ In U (Singleton U x) x1 -> In U X x1
    intros t H'1 H'2; elim H'2; auto with sets.
  Qed.

  Lemma incl_soustr_add_r :
    forall (X:Ensemble U) (x:U),
      ~ In U X x -> Included U X (Subtract U (Add U X x) x).U:Type
forall (X : Ensemble U) (x : U),
~ In U X x -> Included U X (Subtract U (Add U X x) x)
  Proof.U:Type
forall (X : Ensemble U) (x : U),
~ In U X x -> Included U X (Subtract U (Add U X x) x)
    intros X x H'; red.U:Type
X:Ensemble U
x:U
H':~ In U X x
forall x0 : U,
In U X x0 -> In U (Subtract U (Add U X x) x) x0
    intros x0 H'0; try assumption.U:Type
X:Ensemble U
x:U
H':~ In U X x
x0:U
H'0:In U X x0
In U (Subtract U (Add U X x) x) x0
    apply Subtract_intro; auto with sets.U:Type
X:Ensemble U
x:U
H':~ In U X x
x0:U
H'0:In U X x0
x <> x0
    red; intro H'1; apply H'; rewrite H'1; auto with sets.
  Qed.
  Hint Resolve incl_soustr_add_r: sets.

  Lemma add_soustr_2 :
    forall (X:Ensemble U) (x:U),
      In U X x -> Included U X (Add U (Subtract U X x) x).U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Included U X (Add U (Subtract U X x) x)
  Proof.U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Included U X (Add U (Subtract U X x) x)
    intros X x H'; red.U:Type
X:Ensemble U
x:U
H':In U X x
forall x0 : U,
In U X x0 -> In U (Add U (Subtract U X x) x) x0
    intros x0 H'0; try assumption.U:Type
X:Ensemble U
x:U
H':In U X x
x0:U
H'0:In U X x0
In U (Add U (Subtract U X x) x) x0
    elim (classic (x = x0)); intro K; auto with sets.U:Type
X:Ensemble U
x:U
H':In U X x
x0:U
H'0:In U X x0
K:x = x0
In U (Add U (Subtract U X x) x) x0
    elim K; auto with sets.
  Qed.

  Lemma add_soustr_1 :
    forall (X:Ensemble U) (x:U),
      In U X x -> Included U (Add U (Subtract U X x) x) X.U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Included U (Add U (Subtract U X x) x) X
  Proof.U:Type
forall (X : Ensemble U) (x : U),
In U X x -> Included U (Add U (Subtract U X x) x) X
    intros X x H'; red.U:Type
X:Ensemble U
x:U
H':In U X x
forall x0 : U,
In U (Add U (Subtract U X x) 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 (Add U (Subtract U X x) x) x0
forall x1 : U, In U (Subtract U X x) x1 -> In U X x1
U:Type
X:Ensemble U
x:U
H':In U X x
x0:U
H'0:In U (Add U (Subtract U X x) x) x0
forall x1 : U, In U (Singleton U x) x1 -> In U X x1
    intros y H'1; elim H'1; auto with sets.U:Type
X:Ensemble U
x:U
H':In U X x
x0:U
H'0:In U (Add U (Subtract U X x) x) x0
forall x1 : U, In U (Singleton U x) x1 -> In U X x1
    intros t H'1; try assumption.U:Type
X:Ensemble U
x:U
H':In U X x
x0:U
H'0:In U (Add U (Subtract U X x) x) x0
t:U
H'1:In U (Singleton U x) t
In U X t
    rewrite <- (Singleton_inv U x t); auto with sets.
  Qed.

  Lemma add_soustr_xy :
    forall (X:Ensemble U) (x y:U),
      x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.U:Type
forall (X : Ensemble U) (x y : U),
x <> y ->
Subtract U (Add U X x) y = Add U (Subtract U X y) x
  Proof.U:Type
forall (X : Ensemble U) (x y : U),
x <> y ->
Subtract U (Add U X x) y = Add U (Subtract U X y) x
    intros X x y H'; apply Extensionality_Ensembles.U:Type
X:Ensemble U
x, y:U
H':x <> y
Same_set U (Subtract U (Add U X x) y)
  (Add U (Subtract U X y) x)
    split; red.U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Subtract U (Add U X x) y) x0 ->
In U (Add U (Subtract U X y) x) x0
U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    intros x0 H'0; elim H'0; auto with sets.U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
In U (Add U X x) x0 ->
~ In U (Singleton U y) x0 ->
In U (Add U (Subtract U X y) x) x0
U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    intro H'1; elim H'1.U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
forall x1 : U,
In U X x1 ->
~ In U (Singleton U y) x1 ->
In U (Add U (Subtract U X y) x) x1
U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
forall x1 : U,
In U (Singleton U x) x1 ->
~ In U (Singleton U y) x1 ->
In U (Add U (Subtract U X y) x) x1
U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    intros u H'2 H'3; try assumption.U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
u:U
H'2:In U X u
H'3:~ In U (Singleton U y) u
In U (Add U (Subtract U X y) x) u
U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
forall x1 : U,
In U (Singleton U x) x1 ->
~ In U (Singleton U y) x1 ->
In U (Add U (Subtract U X y) x) x1
U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    apply Add_intro1.U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
u:U
H'2:In U X u
H'3:~ In U (Singleton U y) u
In U (Subtract U X y) u
U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
forall x1 : U,
In U (Singleton U x) x1 ->
~ In U (Singleton U y) x1 ->
In U (Add U (Subtract U X y) x) x1
U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    apply Subtract_intro; auto with sets.U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
forall x1 : U,
In U (Singleton U x) x1 ->
~ In U (Singleton U y) x1 ->
In U (Add U (Subtract U X y) x) x1
U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    intros t H'2 H'3; try assumption.U:Type
X:Ensemble U
x, y:U
H':x <> y
x0:U
H'0:In U (Subtract U (Add U X x) y) x0
H'1:In U (Add U X x) x0
t:U
H'2:In U (Singleton U x) t
H'3:~ In U (Singleton U y) t
In U (Add U (Subtract U X y) x) t
U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    elim (Singleton_inv U x t); auto with sets.U:Type
X:Ensemble U
x, y:U
H':x <> y
forall x0 : U,
In U (Add U (Subtract U X y) x) x0 ->
In U (Subtract U (Add U X x) y) x0
    intros u H'2; try assumption.U:Type
X:Ensemble U
x, y:U
H':x <> y
u:U
H'2:In U (Add U (Subtract U X y) x) u
In U (Subtract U (Add U X x) y) u
    elim (Add_inv U (Subtract U X y) x u); auto with sets.U:Type
X:Ensemble U
x, y:U
H':x <> y
u:U
H'2:In U (Add U (Subtract U X y) x) u
In U (Subtract U X y) u ->
In U (Subtract U (Add U X x) y) u
U:Type
X:Ensemble U
x, y:U
H':x <> y
u:U
H'2:In U (Add U (Subtract U X y) x) u
x = u -> In U (Subtract U (Add U X x) y) u
    intro H'0; elim H'0; auto with sets.U:Type
X:Ensemble U
x, y:U
H':x <> y
u:U
H'2:In U (Add U (Subtract U X y) x) u
x = u -> In U (Subtract U (Add U X x) y) u
    intro H'0; rewrite <- H'0; auto with sets.
  Qed.

  Lemma incl_st_add_soustr :
    forall (X Y:Ensemble U) (x:U),
      ~ In U X x ->
      Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).U:Type
forall (X Y : Ensemble U) (x : U),
~ In U X x ->
Strict_Included U (Add U X x) Y ->
Strict_Included U X (Subtract U Y x)
  Proof.U:Type
forall (X Y : Ensemble U) (x : U),
~ In U X x ->
Strict_Included U (Add U X x) Y ->
Strict_Included U X (Subtract U Y x)
    intros X Y x H' H'0; apply sincl_add_x with (x := x); auto using add_soustr_1 with sets.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Strict_Included U (Add U X x)
  (Add U (Subtract U Y x) x)
    split.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Included U (Add U X x) (Add U (Subtract U Y x) x)
U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Add U X x <> Add U (Subtract U Y x) x
    elim H'0.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Included U (Add U X x) Y ->
Add U X x <> Y ->
Included U (Add U X x) (Add U (Subtract U Y x) x)
U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Add U X x <> Add U (Subtract U Y x) x
    intros H'1 H'2.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
H'1:Included U (Add U X x) Y
H'2:Add U X x <> Y
Included U (Add U X x) (Add U (Subtract U Y x) x)
U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Add U X x <> Add U (Subtract U Y x) x
    generalize (Inclusion_is_transitive U).U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
H'1:Included U (Add U X x) Y
H'2:Add U X x <> Y
Transitive (Ensemble U) (Included U) ->
Included U (Add U X x) (Add U (Subtract U Y x) x)
U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Add U X x <> Add U (Subtract U Y x) x
    intro H'4; red in H'4.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
H'1:Included U (Add U X x) Y
H'2:Add U X x <> Y
H'4:forall x0 y z : Ensemble U,
Included U x0 y -> Included U y z -> Included U x0 z
Included U (Add U X x) (Add U (Subtract U Y x) x)
U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Add U X x <> Add U (Subtract U Y x) x
    apply H'4 with (y := Y); auto using add_soustr_2 with sets.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Strict_Included U (Add U X x) Y
Add U X x <> Add U (Subtract U Y x) x
    red in H'0.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'0:Included U (Add U X x) Y /\ Add U X x <> Y
Add U X x <> Add U (Subtract U Y x) x
    elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'1:Included U (Add U X x) Y
H'2:Add U X x <> Y
Add U X x <> Add U (Subtract U Y x) x
    red; intro H'0; apply H'2.U:Type
X, Y:Ensemble U
x:U
H':~ In U X x
H'1:Included U (Add U X x) Y
H'2:Add U X x <> Y
H'0:Add U X x = Add U (Subtract U Y x) x
Add U X x = Y
    rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
  Qed.

  Lemma Sub_Add_new :
    forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.U:Type
forall (X : Ensemble U) (x : U),
~ In U X x -> X = Subtract U (Add U X x) x
  Proof.U:Type
forall (X : Ensemble U) (x : U),
~ In U X x -> X = Subtract U (Add U X x) x
    auto using incl_soustr_add_l with sets.
  Qed.

  Lemma Simplify_add :
    forall (X X0:Ensemble U) (x:U),
      ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.U:Type
forall (X X0 : Ensemble U) (x : U),
~ In U X x ->
~ In U X0 x -> Add U X x = Add U X0 x -> X = X0
  Proof.U:Type
forall (X X0 : Ensemble U) (x : U),
~ In U X x ->
~ In U X0 x -> Add U X x = Add U X0 x -> X = X0
    intros X X0 x H' H'0 H'1; try assumption.U:Type
X, X0:Ensemble U
x:U
H':~ In U X x
H'0:~ In U X0 x
H'1:Add U X x = Add U X0 x
X = X0
    rewrite (Sub_Add_new X x); auto with sets.U:Type
X, X0:Ensemble U
x:U
H':~ In U X x
H'0:~ In U X0 x
H'1:Add U X x = Add U X0 x
Subtract U (Add U X x) x = X0
    rewrite (Sub_Add_new X0 x); auto with sets.U:Type
X, X0:Ensemble U
x:U
H':~ In U X x
H'0:~ In U X0 x
H'1:Add U X x = Add U X0 x
Subtract U (Add U X x) x = Subtract U (Add U X0 x) x
    rewrite H'1; auto with sets.
  Qed.

  Lemma Included_Add :
    forall (X A:Ensemble U) (x:U),
      Included U X (Add U A x) ->
      Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).U:Type
forall (X A : Ensemble U) (x : U),
Included U X (Add U A x) ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
  Proof.U:Type
forall (X A : Ensemble U) (x : U),
Included U X (Add U A x) ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    intros X A x H'0; try assumption.U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    elim (classic (In U X x)).U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    intro H'1; right; try assumption.U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
H'1:In U X x
exists A' : Ensemble U,
  X = Add U A' x /\ Included U A' A
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    exists (Subtract U X x).U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
H'1:In U X x
X = Add U (Subtract U X x) x /\
Included U (Subtract U X x) A
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    split; auto using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 with sets.U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
H'1:In U X x
Included U (Subtract U X x) A
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    red in H'0.U:Type
X, A:Ensemble U
x:U
H'0:forall x0 : U, In U X x0 -> In U (Add U A x) x0
H'1:In U X x
Included U (Subtract U X x) A
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    red.U:Type
X, A:Ensemble U
x:U
H'0:forall x0 : U, In U X x0 -> In U (Add U A x) x0
H'1:In U X x
forall x0 : U, In U (Subtract U X x) x0 -> In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    intros x0 H'2; try assumption.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:In U X x
x0:U
H'2:In U (Subtract U X x) x0
In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    lapply (Subtract_inv U X x x0); auto with sets.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:In U X x
x0:U
H'2:In U (Subtract U X x) x0
In U X x0 /\ x <> x0 -> In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    intro H'3; elim H'3; intros K K'; clear H'3.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:In U X x
x0:U
H'2:In U (Subtract U X x) x0
K:In U X x0
K':x <> x0
In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    lapply (H'0 x0); auto with sets.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:In U X x
x0:U
H'2:In U (Subtract U X x) x0
K:In U X x0
K':x <> x0
In U (Add U A x) x0 -> In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    intro H'3; try assumption.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:In U X x
x0:U
H'2:In U (Subtract U X x) x0
K:In U X x0
K':x <> x0
H'3:In U (Add U A x) x0
In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    lapply (Add_inv U A x x0); auto with sets.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:In U X x
x0:U
H'2:In U (Subtract U X x) x0
K:In U X x0
K':x <> x0
H'3:In U (Add U A x) x0
In U A x0 \/ x = x0 -> In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    intro H'4; elim H'4;
      [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:In U X x
x0:U
H'2:In U (Subtract U X x) x0
K:In U X x0
K':x <> x0
H'3:In U (Add U A x) x0
H'5:x = x0
In U A x0
U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    elim K'; auto with sets.U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
~ In U X x ->
Included U X A \/
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A)
    intro H'1; left; try assumption.U:Type
X, A:Ensemble U
x:U
H'0:Included U X (Add U A x)
H'1:~ In U X x
Included U X A
    red in H'0.U:Type
X, A:Ensemble U
x:U
H'0:forall x0 : U, In U X x0 -> In U (Add U A x) x0
H'1:~ In U X x
Included U X A
    red.U:Type
X, A:Ensemble U
x:U
H'0:forall x0 : U, In U X x0 -> In U (Add U A x) x0
H'1:~ In U X x
forall x0 : U, In U X x0 -> In U A x0
    intros x0 H'2; try assumption.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:~ In U X x
x0:U
H'2:In U X x0
In U A x0
    lapply (H'0 x0); auto with sets.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:~ In U X x
x0:U
H'2:In U X x0
In U (Add U A x) x0 -> In U A x0
    intro H'3; try assumption.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:~ In U X x
x0:U
H'2:In U X x0
H'3:In U (Add U A x) x0
In U A x0
    lapply (Add_inv U A x x0); auto with sets.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:~ In U X x
x0:U
H'2:In U X x0
H'3:In U (Add U A x) x0
In U A x0 \/ x = x0 -> In U A x0
    intro H'4; elim H'4;
      [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:~ In U X x
x0:U
H'2:In U X x0
H'3:In U (Add U A x) x0
H'5:x = x0
In U A x0
    absurd (In U X x0); auto with sets.U:Type
X, A:Ensemble U
x:U
H'0:forall x1 : U, In U X x1 -> In U (Add U A x) x1
H'1:~ In U X x
x0:U
H'2:In U X x0
H'3:In U (Add U A x) x0
H'5:x = x0
~ In U X x0
    rewrite <- H'5; auto with sets.
  Qed.

  Lemma setcover_inv :
    forall A x y:Ensemble U,
      covers (Ensemble U) (Power_set_PO U A) y x ->
      Strict_Included U x y /\
      (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).U:Type
forall A x y : Ensemble U,
covers (Ensemble U) (Power_set_PO U A) y x ->
Strict_Included U x y /\
(forall z : Ensemble U,
 Included U x z -> Included U z y -> x = z \/ z = y)
  Proof.U:Type
forall A x y : Ensemble U,
covers (Ensemble U) (Power_set_PO U A) y x ->
Strict_Included U x y /\
(forall z : Ensemble U,
 Included U x z -> Included U z y -> x = z \/ z = y)
    intros A x y H'; elim H'.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
Strict_Rel_of (Ensemble U) (Power_set_PO U A) x y ->
~
(exists z : Ensemble U,
   Strict_Rel_of (Ensemble U) (Power_set_PO U A) x z /\
   Strict_Rel_of (Ensemble U) (Power_set_PO U A) z y) ->
Strict_Included U x y /\
(forall z : Ensemble U,
 Included U x z -> Included U z y -> x = z \/ z = y)
    unfold Strict_Rel_of; simpl.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
Included U x y /\ x <> y ->
~
(exists z : Ensemble U,
   (Included U x z /\ x <> z) /\
   Included U z y /\ z <> y) ->
Strict_Included U x y /\
(forall z : Ensemble U,
 Included U x z -> Included U z y -> x = z \/ z = y)
    intros H'0 H'1; split; [ auto with sets | idtac ].U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
H'0:Included U x y /\ x <> y
H'1:~
(exists z : Ensemble U,
(Included U x z /\ x <> z) /\ Included U z y /\ z <> y)
forall z : Ensemble U,
Included U x z -> Included U z y -> x = z \/ z = y
    intros z H'2 H'3; try assumption.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
H'0:Included U x y /\ x <> y
H'1:~
(exists z0 : Ensemble U,
(Included U x z0 /\ x <> z0) /\ Included U z0 y /\ z0 <> y)
z:Ensemble U
H'2:Included U x z
H'3:Included U z y
x = z \/ z = y
    elim (classic (x = z)); auto with sets.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
H'0:Included U x y /\ x <> y
H'1:~
(exists z0 : Ensemble U,
(Included U x z0 /\ x <> z0) /\ Included U z0 y /\ z0 <> y)
z:Ensemble U
H'2:Included U x z
H'3:Included U z y
x <> z -> x = z \/ z = y
    intro H'4; right; try assumption.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
H'0:Included U x y /\ x <> y
H'1:~
(exists z0 : Ensemble U,
(Included U x z0 /\ x <> z0) /\ Included U z0 y /\ z0 <> y)
z:Ensemble U
H'2:Included U x z
H'3:Included U z y
H'4:x <> z
z = y
    elim (classic (z = y)); auto with sets.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
H'0:Included U x y /\ x <> y
H'1:~
(exists z0 : Ensemble U,
(Included U x z0 /\ x <> z0) /\ Included U z0 y /\ z0 <> y)
z:Ensemble U
H'2:Included U x z
H'3:Included U z y
H'4:x <> z
z <> y -> z = y
    intro H'5; try assumption.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
H'0:Included U x y /\ x <> y
H'1:~
(exists z0 : Ensemble U,
(Included U x z0 /\ x <> z0) /\ Included U z0 y /\ z0 <> y)
z:Ensemble U
H'2:Included U x z
H'3:Included U z y
H'4:x <> z
H'5:z <> y
z = y
    elim H'1.U:Type
A, x, y:Ensemble U
H':covers (Ensemble U) (Power_set_PO U A) y x
H'0:Included U x y /\ x <> y
H'1:~
(exists z0 : Ensemble U,
(Included U x z0 /\ x <> z0) /\ Included U z0 y /\ z0 <> y)
z:Ensemble U
H'2:Included U x z
H'3:Included U z y
H'4:x <> z
H'5:z <> y
exists z0 : Ensemble U,
  (Included U x z0 /\ x <> z0) /\
  Included U z0 y /\ z0 <> y
    exists z; auto with sets.
  Qed.

  Theorem Add_covers :
    forall A a:Ensemble U,
      Included U a A ->
      forall x:U,
	In U A x ->
	~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.U:Type
forall A a : Ensemble U,
Included U a A ->
forall x : U,
In U A x ->
~ In U a x ->
covers (Ensemble U) (Power_set_PO U A) (Add U a x) a
  Proof.U:Type
forall A a : Ensemble U,
Included U a A ->
forall x : U,
In U A x ->
~ In U a x ->
covers (Ensemble U) (Power_set_PO U A) (Add U a x) a
    intros A a H' x H'0 H'1; try assumption.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
covers (Ensemble U) (Power_set_PO U A) (Add U a x) a
    apply setcover_intro; auto with sets.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
Strict_Included U a (Add U a x)
U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
~
(exists z : Ensemble U,
   Strict_Included U a z /\
   Strict_Included U z (Add U a x))
    red.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
Included U a (Add U a x) /\ a <> Add U a x
U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
~
(exists z : Ensemble U,
   Strict_Included U a z /\
   Strict_Included U z (Add U a x))
    split; [ idtac | red; intro H'2; try exact H'2 ]; auto with sets.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
H'2:a = Add U a x
False
U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
~
(exists z : Ensemble U,
   Strict_Included U a z /\
   Strict_Included U z (Add U a x))
    apply H'1.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
H'2:a = Add U a x
In U a x
U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
~
(exists z : Ensemble U,
   Strict_Included U a z /\
   Strict_Included U z (Add U a x))
    rewrite H'2; auto with sets.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
~
(exists z : Ensemble U,
   Strict_Included U a z /\
   Strict_Included U z (Add U a x))
    red; intro H'2; elim H'2; clear H'2.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
forall x0 : Ensemble U,
Strict_Included U a x0 /\
Strict_Included U x0 (Add U a x) -> False
    intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Strict_Included U a z
H'4:Strict_Included U z (Add U a x)
False
    lapply (Strict_Included_inv U a z); auto with sets; clear H'3.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'4:Strict_Included U z (Add U a x)
Included U a z /\ Inhabited U (Setminus U z a) ->
False
    intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'4:Strict_Included U z (Add U a x)
H'3:Included U a z
forall x0 : U, In U (Setminus U z a) x0 -> False
    intros x0 H'2; elim H'2.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'4:Strict_Included U z (Add U a x)
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
In U z x0 -> ~ In U a x0 -> False
    intros H'5 H'6; try assumption.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'4:Strict_Included U z (Add U a x)
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
False
    generalize H'4; intro K.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'4:Strict_Included U z (Add U a x)
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
False
    red in H'4.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'4:Included U z (Add U a x) /\ z <> Add U a x
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
False
    elim H'4; intros H'8 H'9; red in H'8; clear H'4.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
False
    lapply (H'8 x0); auto with sets.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
In U (Add U a x) x0 -> False
    intro H'7; try assumption.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
False
    elim (Add_inv U a x x0); auto with sets.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
x = x0 -> False
    intro H'15.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
False
    cut (Included U (Add U a x) z).U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
Included U (Add U a x) z -> False
U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
Included U (Add U a x) z
    intro H'10; try assumption.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
H'10:Included U (Add U a x) z
False
U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
Included U (Add U a x) z
    red in K.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Included U z (Add U a x) /\ z <> Add U a x
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
H'10:Included U (Add U a x) z
False
U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
Included U (Add U a x) z
    elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
Included U (Add U a x) z
    rewrite H'15.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
Included U (Add U a x0) z
    red.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x1 : U, In U z x1 -> In U (Add U a x) x1
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
forall x1 : U, In U (Add U a x0) x1 -> In U z x1
    intros x1 H'10; elim H'10; auto with sets.U:Type
A, a:Ensemble U
H':Included U a A
x:U
H'0:In U A x
H'1:~ In U a x
z:Ensemble U
H'3:Included U a z
x0:U
H'2:In U (Setminus U z a) x0
H'5:In U z x0
H'6:~ In U a x0
K:Strict_Included U z (Add U a x)
H'8:forall x2 : U, In U z x2 -> In U (Add U a x) x2
H'9:z <> Add U a x
H'7:In U (Add U a x) x0
H'15:x = x0
x1:U
H'10:In U (Add U a x0) x1
forall x2 : U, In U (Singleton U x0) x2 -> In U z x2
    intros x2 H'11; elim H'11; auto with sets.
  Qed.

  Theorem covers_Add :
    forall A a a':Ensemble U,
      Included U a A ->
      Included U a' A ->
      covers (Ensemble U) (Power_set_PO U A) a' a ->
      exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.U:Type
forall A a a' : Ensemble U,
Included U a A ->
Included U a' A ->
covers (Ensemble U) (Power_set_PO U A) a' a ->
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
  Proof.U:Type
forall A a a' : Ensemble U,
Included U a A ->
Included U a' A ->
covers (Ensemble U) (Power_set_PO U A) a' a ->
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
    intros A a a' H' H'0 H'1; try assumption.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'1:covers (Ensemble U) (Power_set_PO U A) a' a
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
    elim (setcover_inv A a a'); auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'1:covers (Ensemble U) (Power_set_PO U A) a' a
Strict_Included U a a' ->
(forall z : Ensemble U,
 Included U a z -> Included U z a' -> a = z \/ z = a') ->
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
    intros H'6 H'7.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'1:covers (Ensemble U) (Power_set_PO U A) a' a
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
    clear H'1.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
    elim (Strict_Included_inv U a a'); auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
Included U a a' ->
Inhabited U (Setminus U a' a) ->
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
    intros H'5 H'8; elim H'8.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
forall x : U,
In U (Setminus U a' a) x ->
exists x0 : U,
  a' = Add U a x0 /\ In U A x0 /\ ~ In U a x0
    intros x H'1; elim H'1.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
In U a' x ->
~ In U a x ->
exists x0 : U,
  a' = Add U a x0 /\ In U A x0 /\ ~ In U a x0
    intros H'2 H'3; try assumption.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
exists x0 : U,
  a' = Add U a x0 /\ In U A x0 /\ ~ In U a x0
    exists x.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
a' = Add U a x /\ In U A x /\ ~ In U a x
    split; [ try assumption | idtac ].U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
a' = Add U a x
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    clear H'8 H'1.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
a' = Add U a x
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    elim (H'7 (Add U a x)); auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
a = Add U a x -> a' = Add U a x
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
Included U (Add U a x) a'
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    intro H'1.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
H'1:a = Add U a x
a' = Add U a x
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
Included U (Add U a x) a'
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    absurd (a = Add U a x); auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
H'1:a = Add U a x
a <> Add U a x
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
Included U (Add U a x) a'
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    red; intro H'8; try exact H'8.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
H'1, H'8:a = Add U a x
False
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
Included U (Add U a x) a'
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    apply H'3.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
H'1, H'8:a = Add U a x
In U a x
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
Included U (Add U a x) a'
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    rewrite H'8; auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
Included U (Add U a x) a'
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
Included U (Add U a x) a'
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    red.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
forall x0 : U, In U (Add U a x) x0 -> In U a' x0
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    intros x0 H'1; elim H'1; auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
x:U
H'2:In U a' x
H'3:~ In U a x
x0:U
H'1:In U (Add U a x) x0
forall x1 : U, In U (Singleton U x) x1 -> In U a' x1
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    intros x1 H'8; elim H'8; auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x /\ ~ In U a x
    split; [ idtac | try assumption ].U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
H'6:Strict_Included U a a'
H'7:forall z : Ensemble U, Included U a z -> Included U z a' -> a = z \/ z = a'
H'5:Included U a a'
H'8:Inhabited U (Setminus U a' a)
x:U
H'1:In U (Setminus U a' a) x
H'2:In U a' x
H'3:~ In U a x
In U A x
    red in H'0; auto with sets.
  Qed.

  Theorem covers_is_Add :
    forall A a a':Ensemble U,
      Included U a A ->
      Included U a' A ->
      (covers (Ensemble U) (Power_set_PO U A) a' a <->
	(exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).U:Type
forall A a a' : Ensemble U,
Included U a A ->
Included U a' A ->
covers (Ensemble U) (Power_set_PO U A) a' a <->
(exists x : U,
   a' = Add U a x /\ In U A x /\ ~ In U a x)
  Proof.U:Type
forall A a a' : Ensemble U,
Included U a A ->
Included U a' A ->
covers (Ensemble U) (Power_set_PO U A) a' a <->
(exists x : U,
   a' = Add U a x /\ In U A x /\ ~ In U a x)
    intros A a a' H' H'0; split; intro K.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
K:covers (Ensemble U) (Power_set_PO U A) a' a
exists x : U, a' = Add U a x /\ In U A x /\ ~ In U a x
U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
K:exists x : U,
  a' = Add U a x /\ In U A x /\ ~ In U a x
covers (Ensemble U) (Power_set_PO U A) a' a
    apply covers_Add with (A := A); auto with sets.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
K:exists x : U,
  a' = Add U a x /\ In U A x /\ ~ In U a x
covers (Ensemble U) (Power_set_PO U A) a' a
    elim K.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
K:exists x : U,
  a' = Add U a x /\ In U A x /\ ~ In U a x
forall x : U,
a' = Add U a x /\ In U A x /\ ~ In U a x ->
covers (Ensemble U) (Power_set_PO U A) a' a
    intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.U:Type
A, a, a':Ensemble U
H':Included U a A
H'0:Included U a' A
K:exists x0 : U,
  a' = Add U a x0 /\ In U A x0 /\ ~ In U a x0
x:U
H'2:a' = Add U a x
H'3:In U A x /\ ~ In U a x
covers (Ensemble U) (Power_set_PO U A) (Add U a x) a
    apply Add_covers; intuition.
  Qed.

  Theorem Singleton_atomic :
    forall (x:U) (A:Ensemble U),
      In U A x ->
      covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).U:Type
forall (x : U) (A : Ensemble U),
In U A x ->
covers (Ensemble U) (Power_set_PO U A) (Singleton U x)
  (Empty_set U)
  Proof.U:Type
forall (x : U) (A : Ensemble U),
In U A x ->
covers (Ensemble U) (Power_set_PO U A) (Singleton U x)
  (Empty_set U)
    intros x A H'.U:Type
x:U
A:Ensemble U
H':In U A x
covers (Ensemble U) (Power_set_PO U A) (Singleton U x)
  (Empty_set U)
    rewrite <- (Empty_set_zero' U x).U:Type
x:U
A:Ensemble U
H':In U A x
covers (Ensemble U) (Power_set_PO U A)
  (Add U (Empty_set U) x) (Empty_set U)
    apply Add_covers; auto with sets.
  Qed.

  Lemma less_than_singleton :
    forall (X:Ensemble U) (x:U),
      Strict_Included U X (Singleton U x) -> X = Empty_set U.U:Type
forall (X : Ensemble U) (x : U),
Strict_Included U X (Singleton U x) -> X = Empty_set U
  Proof.U:Type
forall (X : Ensemble U) (x : U),
Strict_Included U X (Singleton U x) -> X = Empty_set U
    intros X x H'; try assumption.U:Type
X:Ensemble U
x:U
H':Strict_Included U X (Singleton U x)
X = Empty_set U
    red in H'.U:Type
X:Ensemble U
x:U
H':Included U X (Singleton U x) /\
X <> Singleton U x
X = Empty_set U
    lapply (Singleton_atomic x (Full_set U));
      [ intro H'2; try exact H'2 | apply Full_intro ].U:Type
X:Ensemble U
x:U
H':Included U X (Singleton U x) /\
X <> Singleton U x
H'2:covers (Ensemble U) (Power_set_PO U (Full_set U)) (Singleton U x)
(Empty_set U)
X = Empty_set U
    elim H'; intros H'0 H'1; try exact H'1; clear H'.U:Type
X:Ensemble U
x:U
H'2:covers (Ensemble U) (Power_set_PO U (Full_set U)) (Singleton U x)
(Empty_set U)
H'0:Included U X (Singleton U x)
H'1:X <> Singleton U x
X = Empty_set U
    elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
      [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.U:Type
X:Ensemble U
x:U
H'2:covers (Ensemble U) (Power_set_PO U (Full_set U)) (Singleton U x)
(Empty_set U)
H'0:Included U X (Singleton U x)
H'1:X <> Singleton U x
H'6:Strict_Included U (Empty_set U) (Singleton U x)
H'7:forall z : Ensemble U,
Included U (Empty_set U) z ->
Included U z (Singleton U x) -> Empty_set U = z \/ z = Singleton U x
X = Empty_set U
    elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
      auto with sets.U:Type
X:Ensemble U
x:U
H'2:covers (Ensemble U) (Power_set_PO U (Full_set U)) (Singleton U x)
(Empty_set U)
H'0:Included U X (Singleton U x)
H'1:X <> Singleton U x
H'6:Strict_Included U (Empty_set U) (Singleton U x)
H'7:forall z : Ensemble U,
Included U (Empty_set U) z ->
Included U z (Singleton U x) -> Empty_set U = z \/ z = Singleton U x
H'5:X = Singleton U x
X = Empty_set U
    elim H'1; auto with sets.
  Qed.

End Sets_as_an_algebra.

Hint Resolve incl_soustr_in: sets.
Hint Resolve incl_soustr: sets.
Hint Resolve incl_soustr_add_l: sets.
Hint Resolve incl_soustr_add_r: sets.
Hint Resolve add_soustr_1 add_soustr_2: sets.
Hint Resolve add_soustr_xy: sets.