# 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.

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.

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.