# Library Coq.Sets.Finite_sets_facts

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
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.
Lemma cardinal_finite :
forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
Theorem Add_preserves_Finite :
forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
Theorem Union_preserves_Finite :
forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
Lemma Finite_downward_closed :
forall A:Ensemble U,
Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
Lemma Intersection_preserves_finite :
forall A:Ensemble U,
Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
Lemma cardinalO_empty :
forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
Lemma inh_card_gt_O :
forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
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).
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.
Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
Lemma cardinal_unicity :
forall (X:Ensemble U) (n:nat),
cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
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.
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.
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.
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).
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.
End Finite_sets_facts.