diff options
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, |