Finite_sets_facts.v

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 Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Gt.
Require Export Lt.

Section Finite_sets_facts.
  Variable U : Type.

  Lemma finite_cardinal :
    forall X:Ensemble U, Finite U X ->  exists n : nat, cardinal U X n.U:Type
forall X : Ensemble U,
Finite U X -> exists n : nat, cardinal U X n
  Proof.U:Type
forall X : Ensemble U,
Finite U X -> exists n : nat, cardinal U X n
    induction 1 as [| A _ [n H]].U:Type
exists n : nat, cardinal U (Empty_set U) n
U:Type
A:Ensemble U
n:nat
x:U
H0:~ In U A x
H:cardinal U A n
exists n0 : nat, cardinal U (Add U A x) n0
    exists 0; auto with sets.U:Type
A:Ensemble U
n:nat
x:U
H0:~ In U A x
H:cardinal U A n
exists n0 : nat, cardinal U (Add U A x) n0
    exists (S n); auto with sets.
  Qed.

  Lemma cardinal_finite :
    forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.U:Type
forall (X : Ensemble U) (n : nat),
cardinal U X n -> Finite U X
  Proof.U:Type
forall (X : Ensemble U) (n : nat),
cardinal U X n -> Finite U X
    induction 1; auto with sets.
  Qed.

  Theorem Add_preserves_Finite :
    forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).U:Type
forall (X : Ensemble U) (x : U),
Finite U X -> Finite U (Add U X x)
  Proof.U:Type
forall (X : Ensemble U) (x : U),
Finite U X -> Finite U (Add U X x)
    intros X x H'.U:Type
X:Ensemble U
x:U
H':Finite U X
Finite U (Add U X x)
    elim (classic (In U X x)); intro H'0; auto with sets.U:Type
X:Ensemble U
x:U
H':Finite U X
H'0:In U X x
Finite U (Add U X x)
    rewrite (Non_disjoint_union U X x); auto with sets.
  Qed.

  Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).U:Type
forall x : U, Finite U (Singleton U x)
  Proof.U:Type
forall x : U, Finite U (Singleton U x)
    intro x; rewrite <- (Empty_set_zero U (Singleton U x)).U:Type
x:U
Finite U (Union U (Empty_set U) (Singleton U x))
    change (Finite U (Add U (Empty_set U) x)); auto with sets.
  Qed.

  Theorem Union_preserves_Finite :
    forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).U:Type
forall X Y : Ensemble U,
Finite U X -> Finite U Y -> Finite U (Union U X Y)
  Proof.U:Type
forall X Y : Ensemble U,
Finite U X -> Finite U Y -> Finite U (Union U X Y)
    intros X Y H; induction H as [|A Fin_A Hind x].U:Type
Y:Ensemble U
Finite U Y -> Finite U (Union U (Empty_set U) Y)
U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
Finite U Y -> Finite U (Union U (Add U A x) Y)
    rewrite (Empty_set_zero U Y).U:Type
Y:Ensemble U
Finite U Y -> Finite U Y
U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
Finite U Y -> Finite U (Union U (Add U A x) Y) trivial.U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
Finite U Y -> Finite U (Union U (Add U A x) Y)
    intros.U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
H0:Finite U Y
Finite U (Union U (Add U A x) Y)
    rewrite (Union_commutative U (Add U A x) Y).U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
H0:Finite U Y
Finite U (Union U Y (Add U A x))
    rewrite <- (Union_add U Y A x).U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
H0:Finite U Y
Finite U (Add U (Union U Y A) x)
    rewrite (Union_commutative U Y A).U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
H0:Finite U Y
Finite U (Add U (Union U A Y) x)
    apply Add_preserves_Finite.U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
H0:Finite U Y
Finite U (Union U A Y)
    apply Hind.U:Type
Y, A:Ensemble U
Fin_A:Finite U A
x:U
H:~ In U A x
Hind:Finite U Y -> Finite U (Union U A Y)
H0:Finite U Y
Finite U Y assumption.
  Qed.

  Lemma Finite_downward_closed :
    forall A:Ensemble U,
      Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.U:Type
forall A : Ensemble U,
Finite U A ->
forall X : Ensemble U, Included U X A -> Finite U X
  Proof.U:Type
forall A : Ensemble U,
Finite U A ->
forall X : Ensemble U, Included U X A -> Finite U X
    intros A H'; elim H'; auto with sets.U:Type
A:Ensemble U
H':Finite U A
forall X : Ensemble U,
Included U X (Empty_set U) -> Finite U X
U:Type
A:Ensemble U
H':Finite U A
forall A0 : Ensemble U,
Finite U A0 ->
(forall X : Ensemble U, Included U X A0 -> Finite U X) ->
forall x : U,
~ In U A0 x ->
forall X : Ensemble U,
Included U X (Add U A0 x) -> Finite U X
    intros X H'0.U:Type
A:Ensemble U
H':Finite U A
X:Ensemble U
H'0:Included U X (Empty_set U)
Finite U X
U:Type
A:Ensemble U
H':Finite U A
forall A0 : Ensemble U,
Finite U A0 ->
(forall X : Ensemble U, Included U X A0 -> Finite U X) ->
forall x : U,
~ In U A0 x ->
forall X : Ensemble U,
Included U X (Add U A0 x) -> Finite U X
    rewrite (less_than_empty U X H'0); auto with sets.U:Type
A:Ensemble U
H':Finite U A
forall A0 : Ensemble U,
Finite U A0 ->
(forall X : Ensemble U, Included U X A0 -> Finite U X) ->
forall x : U,
~ In U A0 x ->
forall X : Ensemble U,
Included U X (Add U A0 x) -> Finite U X
    intros; elim Included_Add with U X A0 x; auto with sets.U:Type
A:Ensemble U
H':Finite U A
A0:Ensemble U
H:Finite U A0
H0:forall X0 : Ensemble U,
Included U X0 A0 -> Finite U X0
x:U
H1:~ In U A0 x
X:Ensemble U
H2:Included U X (Add U A0 x)
(exists A' : Ensemble U,
   X = Add U A' x /\ Included U A' A0) -> Finite U X
    destruct 1 as [A' [H5 H6]].U:Type
A:Ensemble U
H':Finite U A
A0:Ensemble U
H:Finite U A0
H0:forall X0 : Ensemble U,
Included U X0 A0 -> Finite U X0
x:U
H1:~ In U A0 x
X:Ensemble U
H2:Included U X (Add U A0 x)
A':Ensemble U
H5:X = Add U A' x
H6:Included U A' A0
Finite U X
    rewrite H5; auto with sets.
  Qed.

  Lemma Intersection_preserves_finite :
    forall A:Ensemble U,
      Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).U:Type
forall A : Ensemble U,
Finite U A ->
forall X : Ensemble U, Finite U (Intersection U X A)
  Proof.U:Type
forall A : Ensemble U,
Finite U A ->
forall X : Ensemble U, Finite U (Intersection U X A)
    intros A H' X; apply Finite_downward_closed with A; auto with sets.
  Qed.

  Lemma cardinalO_empty :
    forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.U:Type
forall X : Ensemble U,
cardinal U X 0 -> X = Empty_set U
  Proof.U:Type
forall X : Ensemble U,
cardinal U X 0 -> X = Empty_set U
    intros X H; apply (cardinal_invert U X 0); trivial with sets.
  Qed.

  Lemma inh_card_gt_O :
    forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.U:Type
forall X : Ensemble U,
Inhabited U X ->
forall n : nat, cardinal U X n -> n > 0
  Proof.U:Type
forall X : Ensemble U,
Inhabited U X ->
forall n : nat, cardinal U X n -> n > 0
    induction 1 as [x H'].U:Type
X:Ensemble U
x:U
H':In U X x
forall n : nat, cardinal U X n -> n > 0
    intros n H'0.U:Type
X:Ensemble U
x:U
H':In U X x
n:nat
H'0:cardinal U X n
n > 0
    elim (gt_O_eq n); auto with sets.U:Type
X:Ensemble U
x:U
H':In U X x
n:nat
H'0:cardinal U X n
0 = n -> n > 0
    intro H'1; generalize H'; generalize H'0.U:Type
X:Ensemble U
x:U
H':In U X x
n:nat
H'0:cardinal U X n
H'1:0 = n
cardinal U X n -> In U X x -> n > 0
    rewrite <- H'1; intro H'2.U:Type
X:Ensemble U
x:U
H':In U X x
n:nat
H'0:cardinal U X n
H'1:0 = n
H'2:cardinal U X 0
In U X x -> 0 > 0
    rewrite (cardinalO_empty X); auto with sets.U:Type
X:Ensemble U
x:U
H':In U X x
n:nat
H'0:cardinal U X n
H'1:0 = n
H'2:cardinal U X 0
In U (Empty_set U) x -> 0 > 0
    intro H'3; elim H'3.
  Qed.

  Lemma card_soustr_1 :
    forall (X:Ensemble U) (n:nat),
      cardinal U X n ->
      forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).U:Type
forall (X : Ensemble U) (n : nat),
cardinal U X n ->
forall x : U,
In U X x -> cardinal U (Subtract U X x) (Nat.pred n)
  Proof.U:Type
forall (X : Ensemble U) (n : nat),
cardinal U X n ->
forall x : U,
In U X x -> cardinal U (Subtract U X x) (Nat.pred n)
    intros X n H'; elim H'.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
forall x : U,
In U (Empty_set U) x ->
cardinal U (Subtract U (Empty_set U) x) (Nat.pred 0)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(forall x : U,
 In U A x -> cardinal U (Subtract U A x) (Nat.pred n0)) ->
forall x : U,
~ In U A x ->
forall x0 : U,
In U (Add U A x) x0 ->
cardinal U (Subtract U (Add U A x) x0)
  (Nat.pred (S n0))
    intros x H'0; elim H'0.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(forall x : U,
 In U A x -> cardinal U (Subtract U A x) (Nat.pred n0)) ->
forall x : U,
~ In U A x ->
forall x0 : U,
In U (Add U A x) x0 ->
cardinal U (Subtract U (Add U A x) x0)
  (Nat.pred (S n0))
    clear H' n X.U:Type
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall x : U,
 In U A x -> cardinal U (Subtract U A x) (Nat.pred n)) ->
forall x : U,
~ In U A x ->
forall x0 : U,
In U (Add U A x) x0 ->
cardinal U (Subtract U (Add U A x) x0)
  (Nat.pred (S n))
    intros X n H' H'0 x H'1 x0 H'2.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    elim (classic (In U X x0)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intro H'4; rewrite (add_soustr_xy U X x x0).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    elim (classic (x = x0)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x = x0 ->
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0 ->
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intro H'5.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'5:x = x0
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0 ->
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    absurd (In U X x0); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'5:x = x0
~ In U X x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0 ->
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    rewrite <- H'5; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0 ->
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intro H'3; try assumption.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    cut (S (pred n) = pred (S n)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
S (Nat.pred n) = Nat.pred (S n) ->
cardinal U (Add U (Subtract U X x0) x)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
S (Nat.pred n) = Nat.pred (S n)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intro H'5; rewrite <- H'5.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
H'5:S (Nat.pred n) = Nat.pred (S n)
cardinal U (Add U (Subtract U X x0) x)
  (S (Nat.pred n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
S (Nat.pred n) = Nat.pred (S n)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    apply card_add; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
H'5:S (Nat.pred n) = Nat.pred (S n)
~ In U (Subtract U X x0) x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
S (Nat.pred n) = Nat.pred (S n)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    red; intro H'6; elim H'6.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
H'5:S (Nat.pred n) = Nat.pred (S n)
H'6:In U (Subtract U X x0) x
In U X x -> ~ In U (Singleton U x0) x -> False
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
S (Nat.pred n) = Nat.pred (S n)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intros H'7 H'8; try assumption.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
H'5:S (Nat.pred n) = Nat.pred (S n)
H'6:In U (Subtract U X x0) x
H'7:In U X x
H'8:~ In U (Singleton U x0) x
False
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
S (Nat.pred n) = Nat.pred (S n)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    elim H'1; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
S (Nat.pred n) = Nat.pred (S n)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    unfold pred at 2; symmetry .U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
n = S (Nat.pred n)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    apply S_pred with (m := 0).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
0 < n
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    change (n > 0).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
n > 0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    apply inh_card_gt_O with (X := X); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x <> x0
Inhabited U X
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    apply Inhabited_intro with (x := x0); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
x <> x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    red; intro H'3.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x = x0
False
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    apply H'1.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x = x0
In U X x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    elim H'3; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'4:In U X x0
H'3:x = x0
In U X x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    rewrite H'3; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    elim (classic (x = x0)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
x = x0 ->
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
x <> x0 ->
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intro H'3; rewrite <- H'3.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'3:x = x0
~ In U X x ->
cardinal U (Subtract U (Add U X x) x) (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
x <> x0 ->
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    cut (Subtract U (Add U X x) x = X); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'3:x = x0
Subtract U (Add U X x) x = X ->
~ In U X x ->
cardinal U (Subtract U (Add U X x) x) (Nat.pred (S n))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
x <> x0 ->
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intro H'4; rewrite H'4; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
x <> x0 ->
~ In U X x0 ->
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    intros H'3 H'4; try assumption.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'3:x <> x0
H'4:~ In U X x0
cardinal U (Subtract U (Add U X x) x0)
  (Nat.pred (S n))
    absurd (In U (Add U X x) x0); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'3:x <> x0
H'4:~ In U X x0
~ In U (Add U X x) x0
    red; intro H'5; try exact H'5.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall x1 : U, In U X x1 -> cardinal U (Subtract U X x1) (Nat.pred n)
x:U
H'1:~ In U X x
x0:U
H'2:In U (Add U X x) x0
H'3:x <> x0
H'4:~ In U X x0
H'5:In U (Add U X x) x0
False
    lapply (Add_inv U X x x0); tauto.
  Qed.

  Lemma cardinal_is_functional :
    forall (X:Ensemble U) (c1:nat),
      cardinal U X c1 ->
      forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.U:Type
forall (X : Ensemble U) (c1 : nat),
cardinal U X c1 ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> X = Y -> c1 = c2
  Proof.U:Type
forall (X : Ensemble U) (c1 : nat),
cardinal U X c1 ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> X = Y -> c1 = c2
    intros X c1 H'; elim H'.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Empty_set U = Y -> 0 = c2
U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> A = Y -> n = c2) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Add U A x = Y -> S n = c2
    intros Y c2 H'0; elim H'0; auto with sets.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
Y:Ensemble U
c2:nat
H'0:cardinal U Y c2
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(Empty_set U = A -> 0 = n) ->
forall x : U,
~ In U A x -> Empty_set U = Add U A x -> 0 = S n
U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> A = Y -> n = c2) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Add U A x = Y -> S n = c2
    intros A n H'1 H'2 x H'3 H'5.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
Y:Ensemble U
c2:nat
H'0:cardinal U Y c2
A:Ensemble U
n:nat
H'1:cardinal U A n
H'2:Empty_set U = A -> 0 = n
x:U
H'3:~ In U A x
H'5:Empty_set U = Add U A x
0 = S n
U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> A = Y -> n = c2) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Add U A x = Y -> S n = c2
    elim (not_Empty_Add U A x); auto with sets.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> A = Y -> n = c2) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Add U A x = Y -> S n = c2
    clear H' c1 X.U:Type
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> A = Y -> n = c2) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Add U A x = Y -> S n = c2
    intros X n H' H'0 x H'1 Y c2 H'2.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat), cardinal U Y0 c0 -> X = Y0 -> n = c0
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
Add U X x = Y -> S n = c2
    elim H'2.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat), cardinal U Y0 c0 -> X = Y0 -> n = c0
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
Add U X x = Empty_set U -> S n = 0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat), cardinal U Y0 c0 -> X = Y0 -> n = c0
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(Add U X x = A -> S n = n0) ->
forall x0 : U,
~ In U A x0 -> Add U X x = Add U A x0 -> S n = S n0
    intro H'3.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat), cardinal U Y0 c0 -> X = Y0 -> n = c0
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
H'3:Add U X x = Empty_set U
S n = 0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat), cardinal U Y0 c0 -> X = Y0 -> n = c0
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(Add U X x = A -> S n = n0) ->
forall x0 : U,
~ In U A x0 -> Add U X x = Add U A x0 -> S n = S n0
    elim (not_Empty_Add U X x); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat), cardinal U Y0 c0 -> X = Y0 -> n = c0
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(Add U X x = A -> S n = n0) ->
forall x0 : U,
~ In U A x0 -> Add U X x = Add U A x0 -> S n = S n0
    clear H'2 c2 Y.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c2 : nat), cardinal U Y c2 -> X = Y -> n = c2
x:U
H'1:~ In U X x
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(Add U X x = A -> S n = n0) ->
forall x0 : U,
~ In U A x0 -> Add U X x = Add U A x0 -> S n = S n0
    intros X0 c2 H'2 H'3 x0 H'4 H'5.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
S n = S c2
    elim (classic (In U X0 x)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
In U X0 x -> S n = S c2
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
~ In U X0 x -> S n = S c2
    intro H'6; apply f_equal.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:In U X0 x
n = c2
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
~ In U X0 x -> S n = S c2
    apply H'0 with (Y := Subtract U (Add U X0 x0) x).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:In U X0 x
cardinal U (Subtract U (Add U X0 x0) x) c2
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:In U X0 x
X = Subtract U (Add U X0 x0) x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
~ In U X0 x -> S n = S c2
    elimtype (pred (S c2) = c2); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:In U X0 x
cardinal U (Subtract U (Add U X0 x0) x)
  (Nat.pred (S c2))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:In U X0 x
X = Subtract U (Add U X0 x0) x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
~ In U X0 x -> S n = S c2
    apply card_soustr_1; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:In U X0 x
X = Subtract U (Add U X0 x0) x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
~ In U X0 x -> S n = S c2
    rewrite <- H'5.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:In U X0 x
X = Subtract U (Add U X x) x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
~ In U X0 x -> S n = S c2
    apply Sub_Add_new; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
~ In U X0 x -> S n = S c2
    elim (classic (x = x0)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
x = x0 -> ~ In U X0 x -> S n = S c2
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
x <> x0 -> ~ In U X0 x -> S n = S c2
    intros H'6 H'7; apply f_equal.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:x = x0
H'7:~ In U X0 x
n = c2
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
x <> x0 -> ~ In U X0 x -> S n = S c2
    apply H'0 with (Y := X0); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:x = x0
H'7:~ In U X0 x
X = X0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
x <> x0 -> ~ In U X0 x -> S n = S c2
    apply Simplify_add with (x := x); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:x = x0
H'7:~ In U X0 x
Add U X x = Add U X0 x
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
x <> x0 -> ~ In U X0 x -> S n = S c2
    pattern x at 2; rewrite H'6; auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
x <> x0 -> ~ In U X0 x -> S n = S c2
    intros H'6 H'7.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
S n = S c2
    absurd (Add U X x = Add U X0 x0); auto with sets.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat), cardinal U Y c0 -> X = Y -> n = c0
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Add U X x = X0 -> S n = c2
x0:U
H'4:~ In U X0 x0
H'5:Add U X x = Add U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
Add U X x <> Add U X0 x0
    clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.U:Type
X:Ensemble U
x:U
X0:Ensemble U
x0:U
H'6:x <> x0
H'7:~ In U X0 x
Add U X x <> Add U X0 x0
    red; intro H'.U:Type
X:Ensemble U
x:U
X0:Ensemble U
x0:U
H'6:x <> x0
H'7:~ In U X0 x
H':Add U X x = Add U X0 x0
False
    lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.U:Type
X:Ensemble U
x:U
X0:Ensemble U
x0:U
H'6:x <> x0
H'7:~ In U X0 x
H':Add U X x = Add U X0 x0
Same_set U (Add U X x) (Add U X0 x0) -> False
    clear H'.U:Type
X:Ensemble U
x:U
X0:Ensemble U
x0:U
H'6:x <> x0
H'7:~ In U X0 x
Same_set U (Add U X x) (Add U X0 x0) -> False
    intro H'; red in H'.U:Type
X:Ensemble U
x:U
X0:Ensemble U
x0:U
H'6:x <> x0
H'7:~ In U X0 x
H':Included U (Add U X x) (Add U X0 x0) /\
Included U (Add U X0 x0) (Add U X x)
False
    elim H'; intros H'0 H'1; red in H'0; clear H' H'1.U:Type
X:Ensemble U
x:U
X0:Ensemble U
x0:U
H'6:x <> x0
H'7:~ In U X0 x
H'0:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
False
    absurd (In U (Add U X0 x0) x); auto with sets.U:Type
X:Ensemble U
x:U
X0:Ensemble U
x0:U
H'6:x <> x0
H'7:~ In U X0 x
H'0:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
~ In U (Add U X0 x0) x
    lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
  Qed.

  Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.U:Type
forall m : nat, cardinal U (Empty_set U) m -> 0 = m
  Proof.U:Type
forall m : nat, cardinal U (Empty_set U) m -> 0 = m
    intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).U:Type
m:nat
Cm:cardinal U (Empty_set U) m
match m with
| 0 => Empty_set U = Empty_set U
| S n =>
    exists (A : Ensemble U) (x : U),
      Empty_set U = Add U A x /\
      ~ In U A x /\ cardinal U A n
end -> 0 = m
    elim m; auto with sets.U:Type
m:nat
Cm:cardinal U (Empty_set U) m
forall n : nat,
(match n with
 | 0 => Empty_set U = Empty_set U
 | S n0 =>
     exists (A : Ensemble U) (x : U),
       Empty_set U = Add U A x /\
       ~ In U A x /\ cardinal U A n0
 end -> 0 = n) ->
(exists (A : Ensemble U) (x : U),
   Empty_set U = Add U A x /\
   ~ In U A x /\ cardinal U A n) -> 0 = S n
    intros; elim H0; intros; elim H1; intros; elim H2; intros.U:Type
m:nat
Cm:cardinal U (Empty_set U) m
n:nat
H:match n with
| 0 => Empty_set U = Empty_set U
| S n0 =>
    exists (A : Ensemble U) (x1 : U),
      Empty_set U = Add U A x1 /\
      ~ In U A x1 /\ cardinal U A n0
end -> 0 = n
H0:exists (A : Ensemble U) (x1 : U),
  Empty_set U = Add U A x1 /\
  ~ In U A x1 /\ cardinal U A n
x:Ensemble U
H1:exists x1 : U,
  Empty_set U = Add U x x1 /\
  ~ In U x x1 /\ cardinal U x n
x0:U
H2:Empty_set U = Add U x x0 /\
~ In U x x0 /\ cardinal U x n
H3:Empty_set U = Add U x x0
H4:~ In U x x0 /\ cardinal U x n
0 = S n
    elim (not_Empty_Add U x x0 H3).
  Qed.

  Lemma cardinal_unicity :
    forall (X:Ensemble U) (n:nat),
      cardinal U X n -> forall m:nat, cardinal U X m -> n = m.U:Type
forall (X : Ensemble U) (n : nat),
cardinal U X n ->
forall m : nat, cardinal U X m -> n = m
  Proof.U:Type
forall (X : Ensemble U) (n : nat),
cardinal U X n ->
forall m : nat, cardinal U X m -> n = m
    intros; apply cardinal_is_functional with X X; auto with sets.
  Qed.

  Lemma card_Add_gen :
    forall (A:Ensemble U) (x:U) (n n':nat),
      cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.U:Type
forall (A : Ensemble U) (x : U) (n n' : nat),
cardinal U A n ->
cardinal U (Add U A x) n' -> n' <= S n
  Proof.U:Type
forall (A : Ensemble U) (x : U) (n n' : nat),
cardinal U A n ->
cardinal U (Add U A x) n' -> n' <= S n
    intros A x n n' H'.U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
cardinal U (Add U A x) n' -> n' <= S n
    elim (classic (In U A x)).U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
In U A x -> cardinal U (Add U A x) n' -> n' <= S n
U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
~ In U A x -> cardinal U (Add U A x) n' -> n' <= S n
    intro H'0.U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:In U A x
cardinal U (Add U A x) n' -> n' <= S n
U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
~ In U A x -> cardinal U (Add U A x) n' -> n' <= S n
    rewrite (Non_disjoint_union U A x H'0).U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:In U A x
cardinal U A n' -> n' <= S n
U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
~ In U A x -> cardinal U (Add U A x) n' -> n' <= S n
    intro H'1; cut (n = n').U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:In U A x
H'1:cardinal U A n'
n = n' -> n' <= S n
U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:In U A x
H'1:cardinal U A n'
n = n'
U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
~ In U A x -> cardinal U (Add U A x) n' -> n' <= S n
    intro E; rewrite E; auto with sets.U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:In U A x
H'1:cardinal U A n'
n = n'
U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
~ In U A x -> cardinal U (Add U A x) n' -> n' <= S n
    apply cardinal_unicity with A; auto with sets.U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
~ In U A x -> cardinal U (Add U A x) n' -> n' <= S n
    intros H'0 H'1.U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:~ In U A x
H'1:cardinal U (Add U A x) n'
n' <= S n
    cut (n' = S n).U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:~ In U A x
H'1:cardinal U (Add U A x) n'
n' = S n -> n' <= S n
U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:~ In U A x
H'1:cardinal U (Add U A x) n'
n' = S n
    intro E; rewrite E; auto with sets.U:Type
A:Ensemble U
x:U
n, n':nat
H':cardinal U A n
H'0:~ In U A x
H'1:cardinal U (Add U A x) n'
n' = S n
    apply cardinal_unicity with (Add U A x); auto with sets.
  Qed.

  Lemma incl_st_card_lt :
    forall (X:Ensemble U) (c1:nat),
      cardinal U X c1 ->
      forall (Y:Ensemble U) (c2:nat),
	cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.U:Type
forall (X : Ensemble U) (c1 : nat),
cardinal U X c1 ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1
  Proof.U:Type
forall (X : Ensemble U) (c1 : nat),
cardinal U X c1 ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1
    intros X c1 H'; elim H'.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 ->
Strict_Included U (Empty_set U) Y -> c2 > 0
U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> Strict_Included U A Y -> c2 > n) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 ->
Strict_Included U (Add U A x) Y -> c2 > S n
    intros Y c2 H'0; elim H'0; auto with sets arith.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
Y:Ensemble U
c2:nat
H'0:cardinal U Y c2
Strict_Included U (Empty_set U) (Empty_set U) -> 0 > 0
U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> Strict_Included U A Y -> c2 > n) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 ->
Strict_Included U (Add U A x) Y -> c2 > S n
    intro H'1.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
Y:Ensemble U
c2:nat
H'0:cardinal U Y c2
H'1:Strict_Included U (Empty_set U) (Empty_set U)
0 > 0
U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> Strict_Included U A Y -> c2 > n) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 ->
Strict_Included U (Add U A x) Y -> c2 > S n
    elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.U:Type
X:Ensemble U
c1:nat
H':cardinal U X c1
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> Strict_Included U A Y -> c2 > n) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 ->
Strict_Included U (Add U A x) Y -> c2 > S n
    clear H' c1 X.U:Type
forall (A : Ensemble U) (n : nat),
cardinal U A n ->
(forall (Y : Ensemble U) (c2 : nat),
 cardinal U Y c2 -> Strict_Included U A Y -> c2 > n) ->
forall x : U,
~ In U A x ->
forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 ->
Strict_Included U (Add U A x) Y -> c2 > S n
    intros X n H' H'0 x H'1 Y c2 H'2.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat),
cardinal U Y0 c0 -> Strict_Included U X Y0 -> c0 > n
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
Strict_Included U (Add U X x) Y -> c2 > S n
    elim H'2.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat),
cardinal U Y0 c0 -> Strict_Included U X Y0 -> c0 > n
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
Strict_Included U (Add U X x) (Empty_set U) -> 0 > S n
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat),
cardinal U Y0 c0 -> Strict_Included U X Y0 -> c0 > n
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(Strict_Included U (Add U X x) A -> n0 > S n) ->
forall x0 : U,
~ In U A x0 ->
Strict_Included U (Add U X x) (Add U A x0) ->
S n0 > S n
    intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y0 : Ensemble U) (c0 : nat),
cardinal U Y0 c0 -> Strict_Included U X Y0 -> c0 > n
x:U
H'1:~ In U X x
Y:Ensemble U
c2:nat
H'2:cardinal U Y c2
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(Strict_Included U (Add U X x) A -> n0 > S n) ->
forall x0 : U,
~ In U A x0 ->
Strict_Included U (Add U X x) (Add U A x0) ->
S n0 > S n
    clear H'2 c2 Y.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c2 : nat),
cardinal U Y c2 -> Strict_Included U X Y -> c2 > n
x:U
H'1:~ In U X x
forall (A : Ensemble U) (n0 : nat),
cardinal U A n0 ->
(Strict_Included U (Add U X x) A -> n0 > S n) ->
forall x0 : U,
~ In U A x0 ->
Strict_Included U (Add U X x) (Add U A x0) ->
S n0 > S n
    intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
In U X0 x -> S c2 > S n
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
~ In U X0 x -> S c2 > S n
    intro H'6; apply gt_n_S.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:In U X0 x
c2 > n
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
~ In U X0 x -> S c2 > S n
    apply H'0 with (Y := Subtract U (Add U X0 x0) x).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:In U X0 x
cardinal U (Subtract U (Add U X0 x0) x) c2
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:In U X0 x
Strict_Included U X (Subtract U (Add U X0 x0) x)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
~ In U X0 x -> S c2 > S n
    elimtype (pred (S c2) = c2); auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:In U X0 x
cardinal U (Subtract U (Add U X0 x0) x)
  (Nat.pred (S c2))
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:In U X0 x
Strict_Included U X (Subtract U (Add U X0 x0) x)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
~ In U X0 x -> S c2 > S n
    apply card_soustr_1; auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:In U X0 x
Strict_Included U X (Subtract U (Add U X0 x0) x)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
~ In U X0 x -> S c2 > S n
    apply incl_st_add_soustr; auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
~ In U X0 x -> S c2 > S n
    elim (classic (x = x0)).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
x = x0 -> ~ In U X0 x -> S c2 > S n
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
x <> x0 -> ~ In U X0 x -> S c2 > S n
    intros H'6 H'7; apply gt_n_S.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:x = x0
H'7:~ In U X0 x
c2 > n
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
x <> x0 -> ~ In U X0 x -> S c2 > S n
    apply H'0 with (Y := X0); auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:x = x0
H'7:~ In U X0 x
Strict_Included U X X0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
x <> x0 -> ~ In U X0 x -> S c2 > S n
    apply sincl_add_x with (x := x0).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:x = x0
H'7:~ In U X0 x
~ In U X x0
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:x = x0
H'7:~ In U X0 x
Strict_Included U (Add U X x0) (Add U X0 x0)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
x <> x0 -> ~ In U X0 x -> S c2 > S n
    rewrite <- H'6; auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
H'6:x = x0
H'7:~ In U X0 x
Strict_Included U (Add U X x0) (Add U X0 x0)
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
x <> x0 -> ~ In U X0 x -> S c2 > S n
    pattern x0 at 1; rewrite <- H'6; trivial with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Strict_Included U (Add U X x) (Add U X0 x0)
x <> x0 -> ~ In U X0 x -> S c2 > S n
    intros H'6 H'7; red in H'5.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'5:Included U (Add U X x) (Add U X0 x0) /\ Add U X x <> Add U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
S c2 > S n
    elim H'5; intros H'8 H'9; try exact H'8; clear H'5.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
H'8:Included U (Add U X x) (Add U X0 x0)
H'9:Add U X x <> Add U X0 x0
S c2 > S n
    red in H'8.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
H'8:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
H'9:Add U X x <> Add U X0 x0
S c2 > S n
    generalize (H'8 x).U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
H'8:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
H'9:Add U X x <> Add U X0 x0
(In U (Add U X x) x -> In U (Add U X0 x0) x) ->
S c2 > S n
    intro H'5; lapply H'5; auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
H'8:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
H'9:Add U X x <> Add U X0 x0
H'5:In U (Add U X x) x -> In U (Add U X0 x0) x
In U (Add U X0 x0) x -> S c2 > S n
    intro H; elim Add_inv with U X0 x0 x; auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
H'8:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
H'9:Add U X x <> Add U X0 x0
H'5:In U (Add U X x) x -> In U (Add U X0 x0) x
H:In U (Add U X0 x0) x
In U X0 x -> S c2 > S n
U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
H'8:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
H'9:Add U X x <> Add U X0 x0
H'5:In U (Add U X x) x -> In U (Add U X0 x0) x
H:In U (Add U X0 x0) x
x0 = x -> S c2 > S n
    intro; absurd (In U X0 x); auto with sets arith.U:Type
X:Ensemble U
n:nat
H':cardinal U X n
H'0:forall (Y : Ensemble U) (c0 : nat),
cardinal U Y c0 -> Strict_Included U X Y -> c0 > n
x:U
H'1:~ In U X x
X0:Ensemble U
c2:nat
H'2:cardinal U X0 c2
H'3:Strict_Included U (Add U X x) X0 -> c2 > S n
x0:U
H'4:~ In U X0 x0
H'6:x <> x0
H'7:~ In U X0 x
H'8:forall x1 : U, In U (Add U X x) x1 -> In U (Add U X0 x0) x1
H'9:Add U X x <> Add U X0 x0
H'5:In U (Add U X x) x -> In U (Add U X0 x0) x
H:In U (Add U X0 x0) x
x0 = x -> S c2 > S n
    intro; absurd (x = x0); auto with sets arith.
  Qed.

  Lemma incl_card_le :
    forall (X Y:Ensemble U) (n m:nat),
      cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.U:Type
forall (X Y : Ensemble U) (n m : nat),
cardinal U X n ->
cardinal U Y m -> Included U X Y -> n <= m
  Proof.U:Type
forall (X Y : Ensemble U) (n m : nat),
cardinal U X n ->
cardinal U Y m -> Included U X Y -> n <= m
    intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:Strict_Included U X Y
n <= m
U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:X = Y
n <= m
    cut (m > n); auto with sets arith.U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:Strict_Included U X Y
m > n
U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:X = Y
n <= m
    apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:X = Y
n <= m
    generalize H0; rewrite <- H2; intro.U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:X = Y
H3:cardinal U X m
n <= m
    cut (n = m).U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:X = Y
H3:cardinal U X m
n = m -> n <= m
U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:X = Y
H3:cardinal U X m
n = m
    intro E; rewrite E; auto with sets arith.U:Type
X, Y:Ensemble U
n, m:nat
H:cardinal U X n
H0:cardinal U Y m
H1:Included U X Y
H2:X = Y
H3:cardinal U X m
n = m
    apply cardinal_unicity with X; auto with sets arith.
  Qed.

  Lemma G_aux :
    forall P:Ensemble U -> Prop,
      (forall X:Ensemble U,
	Finite U X ->
	(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
      P (Empty_set U).U:Type
forall P : Ensemble U -> Prop,
(forall X : Ensemble U,
 Finite U X ->
 (forall Y : Ensemble U, Strict_Included U Y X -> P Y) ->
 P X) -> P (Empty_set U)
  Proof.U:Type
forall P : Ensemble U -> Prop,
(forall X : Ensemble U,
 Finite U X ->
 (forall Y : Ensemble U, Strict_Included U Y X -> P Y) ->
 P X) -> P (Empty_set U)
    intros P H'; try assumption.U:Type
P:Ensemble U -> Prop
H':forall X : Ensemble U,
Finite U X ->
(forall Y : Ensemble U,
 Strict_Included U Y X -> P Y) -> P X
P (Empty_set U)
    apply H'; auto with sets.U:Type
P:Ensemble U -> Prop
H':forall X : Ensemble U,
Finite U X ->
(forall Y : Ensemble U,
 Strict_Included U Y X -> P Y) -> P X
forall Y : Ensemble U,
Strict_Included U Y (Empty_set U) -> P Y
    clear H'; auto with sets.U:Type
P:Ensemble U -> Prop
forall Y : Ensemble U,
Strict_Included U Y (Empty_set U) -> P Y
    intros Y H'; try assumption.U:Type
P:Ensemble U -> Prop
Y:Ensemble U
H':Strict_Included U Y (Empty_set U)
P Y
    red in H'.U:Type
P:Ensemble U -> Prop
Y:Ensemble U
H':Included U Y (Empty_set U) /\ Y <> Empty_set U
P Y
    elim H'; intros H'0 H'1; try exact H'1; clear H'.U:Type
P:Ensemble U -> Prop
Y:Ensemble U
H'0:Included U Y (Empty_set U)
H'1:Y <> Empty_set U
P Y
    lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].U:Type
P:Ensemble U -> Prop
Y:Ensemble U
H'0:Included U Y (Empty_set U)
H'1:Y <> Empty_set U
H'3:Y = Empty_set U
P Y
    elim H'1; auto with sets.
  Qed.

  Lemma Generalized_induction_on_finite_sets :
    forall P:Ensemble U -> Prop,
      (forall X:Ensemble U,
	Finite U X ->
	(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
      forall X:Ensemble U, Finite U X -> P X.U:Type
forall P : Ensemble U -> Prop,
(forall X : Ensemble U,
 Finite U X ->
 (forall Y : Ensemble U, Strict_Included U Y X -> P Y) ->
 P X) -> forall X : Ensemble U, Finite U X -> P X
  Proof.U:Type
forall P : Ensemble U -> Prop,
(forall X : Ensemble U,
 Finite U X ->
 (forall Y : Ensemble U, Strict_Included U Y X -> P Y) ->
 P X) -> forall X : Ensemble U, Finite U X -> P X
    intros P H'0 X H'1.U:Type
P:Ensemble U -> Prop
H'0:forall X0 : Ensemble U,
Finite U X0 -> (forall Y : Ensemble U, Strict_Included U Y X0 -> P Y) -> P X0
X:Ensemble U
H'1:Finite U X
P X
    generalize P H'0; clear H'0 P.U:Type
X:Ensemble U
H'1:Finite U X
forall P : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y : Ensemble U, Strict_Included U Y X0 -> P Y) ->
 P X0) -> P X
    elim H'1.U:Type
X:Ensemble U
H'1:Finite U X
forall P : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y : Ensemble U, Strict_Included U Y X0 -> P Y) ->
 P X0) -> P (Empty_set U)
U:Type
X:Ensemble U
H'1:Finite U X
forall A : Ensemble U,
Finite U A ->
(forall P : Ensemble U -> Prop,
 (forall X0 : Ensemble U,
  Finite U X0 ->
  (forall Y : Ensemble U,
   Strict_Included U Y X0 -> P Y) -> P X0) -> P A) ->
forall x : U,
~ In U A x ->
forall P : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y : Ensemble U, Strict_Included U Y X0 -> P Y) ->
 P X0) -> P (Add U A x)
    intros P H'0.U:Type
X:Ensemble U
H'1:Finite U X
P:Ensemble U -> Prop
H'0:forall X0 : Ensemble U,
Finite U X0 -> (forall Y : Ensemble U, Strict_Included U Y X0 -> P Y) -> P X0
P (Empty_set U)
U:Type
X:Ensemble U
H'1:Finite U X
forall A : Ensemble U,
Finite U A ->
(forall P : Ensemble U -> Prop,
 (forall X0 : Ensemble U,
  Finite U X0 ->
  (forall Y : Ensemble U,
   Strict_Included U Y X0 -> P Y) -> P X0) -> P A) ->
forall x : U,
~ In U A x ->
forall P : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y : Ensemble U, Strict_Included U Y X0 -> P Y) ->
 P X0) -> P (Add U A x)
    apply G_aux; auto with sets.U:Type
X:Ensemble U
H'1:Finite U X
forall A : Ensemble U,
Finite U A ->
(forall P : Ensemble U -> Prop,
 (forall X0 : Ensemble U,
  Finite U X0 ->
  (forall Y : Ensemble U,
   Strict_Included U Y X0 -> P Y) -> P X0) -> P A) ->
forall x : U,
~ In U A x ->
forall P : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y : Ensemble U, Strict_Included U Y X0 -> P Y) ->
 P X0) -> P (Add U A x)
    clear H'1 X.U:Type
forall A : Ensemble U,
Finite U A ->
(forall P : Ensemble U -> Prop,
 (forall X : Ensemble U,
  Finite U X ->
  (forall Y : Ensemble U, Strict_Included U Y X -> P Y) ->
  P X) -> P A) ->
forall x : U,
~ In U A x ->
forall P : Ensemble U -> Prop,
(forall X : Ensemble U,
 Finite U X ->
 (forall Y : Ensemble U, Strict_Included U Y X -> P Y) ->
 P X) -> P (Add U A x)
    intros A H' H'0 x H'1 P H'3.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P0 Y) -> P0 X) ->
P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P Y) -> P X
P (Add U A x)
    cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P0 Y) -> P0 X) ->
P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P Y) -> P X
forall Y : Ensemble U, Included U Y (Add U A x) -> P Y
    generalize H'1.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P0 Y) -> P0 X) ->
P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P Y) -> P X
~ In U A x ->
forall Y : Ensemble U, Included U Y (Add U A x) -> P Y
    apply H'0.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P0 Y) -> P0 X) ->
P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X : Ensemble U,
Finite U X -> (forall Y : Ensemble U, Strict_Included U Y X -> P Y) -> P X
forall X : Ensemble U,
Finite U X ->
(forall Y : Ensemble U,
 Strict_Included U Y X ->
 ~ In U Y x ->
 forall Y0 : Ensemble U,
 Included U Y0 (Add U Y x) -> P Y0) ->
~ In U X x ->
forall Y : Ensemble U, Included U Y (Add U X x) -> P Y
    intros X K H'5 L Y H'6; apply H'3; auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y0 : Ensemble U, Strict_Included U Y0 X0 -> P0 Y0) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y0 : Ensemble U, Strict_Included U Y0 X0 -> P Y0) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y0 : Ensemble U,
Strict_Included U Y0 X ->
~ In U Y0 x -> forall Y1 : Ensemble U, Included U Y1 (Add U Y0 x) -> P Y1
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Finite U Y
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y0 : Ensemble U, Strict_Included U Y0 X0 -> P0 Y0) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y0 : Ensemble U, Strict_Included U Y0 X0 -> P Y0) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y0 : Ensemble U,
Strict_Included U Y0 X ->
~ In U Y0 x -> forall Y1 : Ensemble U, Included U Y1 (Add U Y0 x) -> P Y1
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
forall Y0 : Ensemble U, Strict_Included U Y0 Y -> P Y0
    apply Finite_downward_closed with (A := Add U X x); auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y0 : Ensemble U, Strict_Included U Y0 X0 -> P0 Y0) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y0 : Ensemble U, Strict_Included U Y0 X0 -> P Y0) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y0 : Ensemble U,
Strict_Included U Y0 X ->
~ In U Y0 x -> forall Y1 : Ensemble U, Included U Y1 (Add U Y0 x) -> P Y1
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
forall Y0 : Ensemble U, Strict_Included U Y0 Y -> P Y0
    intros Y0 H'7.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
P Y0
    elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
      auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
Included U Y0 (Add U X x) -> Y0 <> Add U X x -> P Y0
    intros H'2 H'4.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
P Y0
    elim (Included_Add U Y0 X x);
      [ intro H'14
	| intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
	| idtac ]; auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
H'14:Included U Y0 X
P Y0
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
P Y0
    elim (Included_Strict_Included U Y0 X); auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
H'14:Included U Y0 X
Strict_Included U Y0 X -> P Y0
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
H'14:Included U Y0 X
Y0 = X -> P Y0
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
P Y0
    intro H'9; apply H'5 with (Y := Y0); auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
H'14:Included U Y0 X
Y0 = X -> P Y0
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
P Y0
    intro H'9; rewrite H'9.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
H'14:Included U Y0 X
H'9:Y0 = X
P X
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
P Y0
    apply H'3; auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
H'14:Included U Y0 X
H'9:Y0 = X
forall Y1 : Ensemble U, Strict_Included U Y1 X -> P Y1
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
P Y0
    intros Y1 H'8; elim H'8.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y2 : Ensemble U, Strict_Included U Y2 X0 -> P0 Y2) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y2 : Ensemble U, Strict_Included U Y2 X0 -> P Y2) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y2 : Ensemble U,
Strict_Included U Y2 X ->
~ In U Y2 x -> forall Y3 : Ensemble U, Included U Y3 (Add U Y2 x) -> P Y3
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
H'14:Included U Y0 X
H'9:Y0 = X
Y1:Ensemble U
H'8:Strict_Included U Y1 X
Included U Y1 X -> Y1 <> X -> P Y1
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
P Y0
    intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
P Y0
    elim (Included_Strict_Included U A' X); auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
Strict_Included U A' X -> P Y0
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
A' = X -> P Y0
    intro H'8; apply H'5 with (Y := A'); auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
H'8:Strict_Included U A' X
Included U Y0 (Add U A' x)
U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
 Finite U X0 ->
 (forall Y1 : Ensemble U,
  Strict_Included U Y1 X0 -> P0 Y1) -> 
 P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U,
 Strict_Included U Y1 X0 -> P Y1) -> 
P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x ->
forall Y2 : Ensemble U,
Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
A' = X -> P Y0
    rewrite <- H'15; auto with sets.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
A' = X -> P Y0
    intro H'8.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
H'8:A' = X
P Y0
    elim H'7.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
H'8:A' = X
Included U Y0 Y -> Y0 <> Y -> P Y0
    intros H'9 H'10; apply H'10 || elim H'10; try assumption.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
H'8:A' = X
H'9:Included U Y0 Y
H'10:Y0 <> Y
Y0 = Y
    generalize H'6.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
H'8:A' = X
H'9:Included U Y0 Y
H'10:Y0 <> Y
Included U Y (Add U X x) -> Y0 = Y
    rewrite <- H'8.U:Type
A:Ensemble U
H':Finite U A
H'0:forall P0 : Ensemble U -> Prop,
(forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P0 Y1) -> P0 X0) -> P0 A
x:U
H'1:~ In U A x
P:Ensemble U -> Prop
H'3:forall X0 : Ensemble U,
Finite U X0 ->
(forall Y1 : Ensemble U, Strict_Included U Y1 X0 -> P Y1) -> P X0
X:Ensemble U
K:Finite U X
H'5:forall Y1 : Ensemble U,
Strict_Included U Y1 X ->
~ In U Y1 x -> forall Y2 : Ensemble U, Included U Y2 (Add U Y1 x) -> P Y2
L:~ In U X x
Y:Ensemble U
H'6:Included U Y (Add U X x)
Y0:Ensemble U
H'7:Strict_Included U Y0 Y
H'2:Included U Y0 (Add U X x)
H'4:Y0 <> Add U X x
A':Ensemble U
H'15:Y0 = Add U A' x
H'16:Included U A' X
H'8:A' = X
H'9:Included U Y0 Y
H'10:Y0 <> Y
Included U Y (Add U A' x) -> Y0 = Y
    rewrite <- H'15; auto with sets.
  Qed.

End Finite_sets_facts.