diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Sets/Finite_sets_facts.v | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Sets/Finite_sets_facts.v')
| -rw-r--r-- | theories/Sets/Finite_sets_facts.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 91717f9e..fdcc4150 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 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) Require Export Finite_sets. Require Export Constructive_sets. @@ -72,7 +72,7 @@ Section Finite_sets_facts. Proof. intros X Y H; induction H as [|A Fin_A Hind x]. rewrite (Empty_set_zero U Y). trivial. - intros. + intros. rewrite (Union_commutative U (Add U A x) Y). rewrite <- (Union_add U Y A x). rewrite (Union_commutative U Y A). @@ -98,7 +98,7 @@ Section Finite_sets_facts. 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. @@ -212,7 +212,7 @@ Section Finite_sets_facts. 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. @@ -279,7 +279,7 @@ Section Finite_sets_facts. 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, |