summaryrefslogtreecommitdiff
path: root/theories/Sets/Finite_sets_facts.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /theories/Sets/Finite_sets_facts.v
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Sets/Finite_sets_facts.v')
-rw-r--r--theories/Sets/Finite_sets_facts.v583
1 files changed, 290 insertions, 293 deletions
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index ddbf62e4..91717f9e 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Finite_sets_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Finite_sets_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -37,311 +37,308 @@ Require Export Gt.
Require Export Lt.
Section Finite_sets_facts.
-Variable U : Type.
+ Variable U : Type.
-Lemma finite_cardinal :
- forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.
-Proof.
-induction 1 as [| A _ [n H]].
-exists 0; auto with sets.
-exists (S n); auto with sets.
-Qed.
+ Lemma finite_cardinal :
+ forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.
+ Proof.
+ induction 1 as [| A _ [n H]].
+ exists 0; auto with sets.
+ exists (S n); auto with sets.
+ Qed.
-Lemma cardinal_finite :
- forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
-Proof.
-induction 1; auto with sets.
-Qed.
+ Lemma cardinal_finite :
+ forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
+ Proof.
+ 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).
-Proof.
-intros X x H'.
-elim (classic (In U X x)); intro H'0; auto with sets.
-rewrite (Non_disjoint_union U X x); auto with sets.
-Qed.
-Hint Resolve Add_preserves_Finite.
+ Theorem Add_preserves_Finite :
+ forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
+ Proof.
+ intros X x H'.
+ elim (classic (In U X x)); intro H'0; auto with sets.
+ rewrite (Non_disjoint_union U X x); auto with sets.
+ Qed.
-Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
-Proof.
-intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
-change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
-Qed.
-Hint Resolve Singleton_is_finite.
+ Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
+ Proof.
+ intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
+ change (Finite U (Add U (Empty_set U) x)) in |- *; 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).
-Proof.
-intros X Y H'; elim H'.
-rewrite (Empty_set_zero U Y); auto with sets.
-intros A H'0 H'1 x H'2 H'3.
-rewrite (Union_commutative U (Add U A x) Y).
-rewrite <- (Union_add U Y A x).
-rewrite (Union_commutative U Y A); 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).
+ Proof.
+ intros X Y H; induction H as [|A Fin_A Hind x].
+ rewrite (Empty_set_zero U Y). trivial.
+ intros.
+ rewrite (Union_commutative U (Add U A x) Y).
+ rewrite <- (Union_add U Y A x).
+ rewrite (Union_commutative U Y A).
+ apply Add_preserves_Finite.
+ apply Hind. assumption.
+ Qed.
-Lemma Finite_downward_closed :
- forall A:Ensemble U,
- Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
-Proof.
-intros A H'; elim H'; auto with sets.
-intros X H'0.
-rewrite (less_than_empty U X H'0); auto with sets.
-intros; elim Included_Add with U X A0 x; auto with sets.
-destruct 1 as [A' [H5 H6]].
-rewrite H5; auto with sets.
-Qed.
+ Lemma Finite_downward_closed :
+ forall A:Ensemble U,
+ Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
+ Proof.
+ intros A H'; elim H'; auto with sets.
+ intros X H'0.
+ rewrite (less_than_empty U X H'0); auto with sets.
+ intros; elim Included_Add with U X A0 x; auto with sets.
+ destruct 1 as [A' [H5 H6]].
+ 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).
-Proof.
-intros A H' X; apply Finite_downward_closed with A; 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).
+ Proof.
+ 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.
+ Proof.
+ intros X H; apply (cardinal_invert U X 0); trivial with sets.
+ Qed.
-Lemma cardinalO_empty :
- forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
-Proof.
-intros X H; apply (cardinal_invert U X 0); trivial with sets.
-Qed.
-Hint Resolve cardinalO_empty.
+ Lemma inh_card_gt_O :
+ forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
+ Proof.
+ induction 1 as [x H'].
+ intros n H'0.
+ elim (gt_O_eq n); auto with sets.
+ intro H'1; generalize H'; generalize H'0.
+ rewrite <- H'1; intro H'2.
+ rewrite (cardinalO_empty X); auto with sets.
+ intro H'3; elim H'3.
+ Qed.
-Lemma inh_card_gt_O :
- forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
-Proof.
-induction 1 as [x H'].
-intros n H'0.
-elim (gt_O_eq n); auto with sets.
-intro H'1; generalize H'; generalize H'0.
-rewrite <- H'1; intro H'2.
-rewrite (cardinalO_empty X); auto with sets.
-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).
+ Proof.
+ intros X n H'; elim H'.
+ intros x H'0; elim H'0.
+ clear H' n X.
+ intros X n H' H'0 x H'1 x0 H'2.
+ elim (classic (In U X x0)).
+ intro H'4; rewrite (add_soustr_xy U X x x0).
+ elim (classic (x = x0)).
+ intro H'5.
+ absurd (In U X x0); auto with sets.
+ rewrite <- H'5; auto with sets.
+ intro H'3; try assumption.
+ cut (S (pred n) = pred (S n)).
+ intro H'5; rewrite <- H'5.
+ apply card_add; auto with sets.
+ red in |- *; intro H'6; elim H'6.
+ intros H'7 H'8; try assumption.
+ elim H'1; auto with sets.
+ unfold pred at 2 in |- *; symmetry in |- *.
+ apply S_pred with (m := 0).
+ change (n > 0) in |- *.
+ apply inh_card_gt_O with (X := X); auto with sets.
+ apply Inhabited_intro with (x := x0); auto with sets.
+ red in |- *; intro H'3.
+ apply H'1.
+ elim H'3; auto with sets.
+ rewrite H'3; auto with sets.
+ elim (classic (x = x0)).
+ intro H'3; rewrite <- H'3.
+ cut (Subtract U (Add U X x) x = X); auto with sets.
+ intro H'4; rewrite H'4; auto with sets.
+ intros H'3 H'4; try assumption.
+ absurd (In U (Add U X x) x0); auto with sets.
+ red in |- *; intro H'5; try exact H'5.
+ lapply (Add_inv U X x x0); tauto.
+ 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).
-Proof.
-intros X n H'; elim H'.
-intros x H'0; elim H'0.
-clear H' n X.
-intros X n H' H'0 x H'1 x0 H'2.
-elim (classic (In U X x0)).
-intro H'4; rewrite (add_soustr_xy U X x x0).
-elim (classic (x = x0)).
-intro H'5.
-absurd (In U X x0); auto with sets.
-rewrite <- H'5; auto with sets.
-intro H'3; try assumption.
-cut (S (pred n) = pred (S n)).
-intro H'5; rewrite <- H'5.
-apply card_add; auto with sets.
-red in |- *; intro H'6; elim H'6.
-intros H'7 H'8; try assumption.
-elim H'1; auto with sets.
-unfold pred at 2 in |- *; symmetry in |- *.
-apply S_pred with (m := 0).
-change (n > 0) in |- *.
-apply inh_card_gt_O with (X := X); auto with sets.
-apply Inhabited_intro with (x := x0); auto with sets.
-red in |- *; intro H'3.
-apply H'1.
-elim H'3; auto with sets.
-rewrite H'3; auto with sets.
-elim (classic (x = x0)).
-intro H'3; rewrite <- H'3.
-cut (Subtract U (Add U X x) x = X); auto with sets.
-intro H'4; rewrite H'4; auto with sets.
-intros H'3 H'4; try assumption.
-absurd (In U (Add U X x) x0); auto with sets.
-red in |- *; intro H'5; try exact H'5.
-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.
+ Proof.
+ intros X c1 H'; elim H'.
+ intros Y c2 H'0; elim H'0; auto with sets.
+ intros A n H'1 H'2 x H'3 H'5.
+ elim (not_Empty_Add U A x); auto with sets.
+ clear H' c1 X.
+ intros X n H' H'0 x H'1 Y c2 H'2.
+ elim H'2.
+ intro H'3.
+ elim (not_Empty_Add U X x); auto with sets.
+ clear H'2 c2 Y.
+ intros X0 c2 H'2 H'3 x0 H'4 H'5.
+ elim (classic (In U X0 x)).
+ intro H'6; apply f_equal with nat.
+ apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+ elimtype (pred (S c2) = c2); auto with sets.
+ apply card_soustr_1; auto with sets.
+ rewrite <- H'5.
+ apply Sub_Add_new; auto with sets.
+ elim (classic (x = x0)).
+ intros H'6 H'7; apply f_equal with nat.
+ apply H'0 with (Y := X0); auto with sets.
+ apply Simplify_add with (x := x); auto with sets.
+ pattern x at 2 in |- *; rewrite H'6; auto with sets.
+ intros H'6 H'7.
+ absurd (Add U X x = Add U X0 x0); auto with sets.
+ clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
+ red in |- *; intro H'.
+ lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
+ clear H'.
+ intro H'; red in H'.
+ elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
+ absurd (In U (Add U X0 x0) x); auto with sets.
+ lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
+ 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.
-Proof.
-intros X c1 H'; elim H'.
-intros Y c2 H'0; elim H'0; auto with sets.
-intros A n H'1 H'2 x H'3 H'5.
-elim (not_Empty_Add U A x); auto with sets.
-clear H' c1 X.
-intros X n H' H'0 x H'1 Y c2 H'2.
-elim H'2.
-intro H'3.
-elim (not_Empty_Add U X x); auto with sets.
-clear H'2 c2 Y.
-intros X0 c2 H'2 H'3 x0 H'4 H'5.
-elim (classic (In U X0 x)).
-intro H'6; apply f_equal with nat.
-apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-elimtype (pred (S c2) = c2); auto with sets.
-apply card_soustr_1; auto with sets.
-rewrite <- H'5.
-apply Sub_Add_new; auto with sets.
-elim (classic (x = x0)).
-intros H'6 H'7; apply f_equal with nat.
-apply H'0 with (Y := X0); auto with sets.
-apply Simplify_add with (x := x); auto with sets.
-pattern x at 2 in |- *; rewrite H'6; auto with sets.
-intros H'6 H'7.
-absurd (Add U X x = Add U X0 x0); auto with sets.
-clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
-red in |- *; intro H'.
-lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
-clear H'.
-intro H'; red in H'.
-elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
-absurd (In U (Add U X0 x0) x); auto with sets.
-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.
+ Proof.
+ intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
+ elim m; auto with sets.
+ intros; elim H0; intros; elim H1; intros; elim H2; intros.
+ elim (not_Empty_Add U x x0 H3).
+ Qed.
-Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
-Proof.
-intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
-elim m; auto with sets.
-intros; elim H0; intros; elim H1; intros; elim H2; intros.
-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.
+ Proof.
+ 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.
+ Proof.
+ intros A x n n' H'.
+ elim (classic (In U A x)).
+ intro H'0.
+ rewrite (Non_disjoint_union U A x H'0).
+ intro H'1; cut (n = n').
+ intro E; rewrite E; auto with sets.
+ apply cardinal_unicity with A; auto with sets.
+ intros H'0 H'1.
+ cut (n' = S n).
+ intro E; rewrite E; auto with sets.
+ apply cardinal_unicity with (Add U A x); auto with sets.
+ Qed.
-Lemma cardinal_unicity :
- forall (X:Ensemble U) (n:nat),
- cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
-Proof.
-intros; apply cardinal_is_functional with X 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.
+ Proof.
+ intros X c1 H'; elim H'.
+ intros Y c2 H'0; elim H'0; auto with sets arith.
+ intro H'1.
+ elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
+ clear H' c1 X.
+ intros X n H' H'0 x H'1 Y c2 H'2.
+ elim H'2.
+ intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
+ clear H'2 c2 Y.
+ intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
+ intro H'6; apply gt_n_S.
+ apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+ elimtype (pred (S c2) = c2); auto with sets arith.
+ apply card_soustr_1; auto with sets arith.
+ apply incl_st_add_soustr; auto with sets arith.
+ elim (classic (x = x0)).
+ intros H'6 H'7; apply gt_n_S.
+ apply H'0 with (Y := X0); auto with sets arith.
+ apply sincl_add_x with (x := x0).
+ rewrite <- H'6; auto with sets arith.
+ pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
+ intros H'6 H'7; red in H'5.
+ elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
+ red in H'8.
+ generalize (H'8 x).
+ intro H'5; lapply H'5; auto with sets arith.
+ intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
+ intro; absurd (In U X0 x); auto with sets arith.
+ intro; absurd (x = x0); auto with sets arith.
+ 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.
-Proof.
-intros A x n n' H'.
-elim (classic (In U A x)).
-intro H'0.
-rewrite (Non_disjoint_union U A x H'0).
-intro H'1; cut (n = n').
-intro E; rewrite E; auto with sets.
-apply cardinal_unicity with A; auto with sets.
-intros H'0 H'1.
-cut (n' = S n).
-intro E; rewrite E; auto with sets.
-apply cardinal_unicity with (Add U A x); auto with sets.
-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.
+ Proof.
+ intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
+ cut (m > n); auto with sets arith.
+ apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
+ generalize H0; rewrite <- H2; intro.
+ cut (n = m).
+ intro E; rewrite E; auto with sets arith.
+ 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).
+ Proof.
+ intros P H'; try assumption.
+ apply H'; auto with sets.
+ clear H'; auto with sets.
+ intros Y H'; try assumption.
+ red in H'.
+ elim H'; intros H'0 H'1; try exact H'1; clear H'.
+ lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
+ elim H'1; 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.
-Proof.
-intros X c1 H'; elim H'.
-intros Y c2 H'0; elim H'0; auto with sets arith.
-intro H'1.
-elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
-clear H' c1 X.
-intros X n H' H'0 x H'1 Y c2 H'2.
-elim H'2.
-intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
-clear H'2 c2 Y.
-intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
-intro H'6; apply gt_n_S.
-apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-elimtype (pred (S c2) = c2); auto with sets arith.
-apply card_soustr_1; auto with sets arith.
-apply incl_st_add_soustr; auto with sets arith.
-elim (classic (x = x0)).
-intros H'6 H'7; apply gt_n_S.
-apply H'0 with (Y := X0); auto with sets arith.
-apply sincl_add_x with (x := x0).
-rewrite <- H'6; auto with sets arith.
-pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
-intros H'6 H'7; red in H'5.
-elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
-red in H'8.
-generalize (H'8 x).
-intro H'5; lapply H'5; auto with sets arith.
-intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
-intro; absurd (In U X0 x); auto with sets arith.
-intro; absurd (x = x0); auto with sets arith.
-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.
+ Proof.
+ intros P H'0 X H'1.
+ generalize P H'0; clear H'0 P.
+ elim H'1.
+ intros P H'0.
+ apply G_aux; auto with sets.
+ clear H'1 X.
+ intros A H' H'0 x H'1 P H'3.
+ cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
+ generalize H'1.
+ apply H'0.
+ intros X K H'5 L Y H'6; apply H'3; auto with sets.
+ apply Finite_downward_closed with (A := Add U X x); auto with sets.
+ intros Y0 H'7.
+ elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
+ auto with sets.
+ intros H'2 H'4.
+ 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.
+ elim (Included_Strict_Included U Y0 X); auto with sets.
+ intro H'9; apply H'5 with (Y := Y0); auto with sets.
+ intro H'9; rewrite H'9.
+ apply H'3; auto with sets.
+ intros Y1 H'8; elim H'8.
+ intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
+ elim (Included_Strict_Included U A' X); auto with sets.
+ intro H'8; apply H'5 with (Y := A'); auto with sets.
+ rewrite <- H'15; auto with sets.
+ intro H'8.
+ elim H'7.
+ intros H'9 H'10; apply H'10 || elim H'10; try assumption.
+ generalize H'6.
+ rewrite <- H'8.
+ rewrite <- H'15; auto with sets.
+ 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.
-Proof.
-intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
-cut (m > n); auto with sets arith.
-apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
-generalize H0; rewrite <- H2; intro.
-cut (n = m).
-intro E; rewrite E; auto with sets arith.
-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).
-Proof.
-intros P H'; try assumption.
-apply H'; auto with sets.
-clear H'; auto with sets.
-intros Y H'; try assumption.
-red in H'.
-elim H'; intros H'0 H'1; try exact H'1; clear H'.
-lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
-elim H'1; auto with sets.
-Qed.
-
-Hint Unfold not.
-
-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.
-Proof.
-intros P H'0 X H'1.
-generalize P H'0; clear H'0 P.
-elim H'1.
-intros P H'0.
-apply G_aux; auto with sets.
-clear H'1 X.
-intros A H' H'0 x H'1 P H'3.
-cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
-generalize H'1.
-apply H'0.
-intros X K H'5 L Y H'6; apply H'3; auto with sets.
-apply Finite_downward_closed with (A := Add U X x); auto with sets.
-intros Y0 H'7.
-elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
- auto with sets.
-intros H'2 H'4.
-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.
-elim (Included_Strict_Included U Y0 X); auto with sets.
-intro H'9; apply H'5 with (Y := Y0); auto with sets.
-intro H'9; rewrite H'9.
-apply H'3; auto with sets.
-intros Y1 H'8; elim H'8.
-intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
-elim (Included_Strict_Included U A' X); auto with sets.
-intro H'8; apply H'5 with (Y := A'); auto with sets.
-rewrite <- H'15; auto with sets.
-intro H'8.
-elim H'7.
-intros H'9 H'10; apply H'10 || elim H'10; try assumption.
-generalize H'6.
-rewrite <- H'8.
-rewrite <- H'15; auto with sets.
-Qed.
-
-End Finite_sets_facts. \ No newline at end of file
+End Finite_sets_facts.