Library Coqtail.Sets.My_Finite_sets_facts

Require Export Finite_sets.
Require Export My_Sets_facts.
Require Export Arith.

Section Finite_sets_facts.

Implicit Arguments Union [U].
Implicit Arguments Add [U].
Implicit Arguments Singleton [U].
Implicit Arguments Finite [U].
Implicit Arguments cardinal [U].
Implicit Arguments Disjoint [U].

Variable U:Type.

Lemma cardinal_of_disjoint_union : ∀ X:Ensemble U, ∀ n:nat,
  cardinal X n → ∀ Y:Ensemble U, ∀ m:nat,
  cardinal Y m → Disjoint X Y → cardinal (Union X Y) (n+m).
Proof.
induction 1.
intros.
rewrite Union_empty_set_left.
rewrite plus_0_l.
auto.

intros.
rewrite Union_add_left.
simpl.
constructor.
apply IHcardinal.
auto.
apply Disjoint_downward_closed with (Add A x).
auto.
unfold Add.
apply included_in_union.
intro.
destruct H2.
apply H2 with x.
split.
apply Union_intror.
constructor.
destruct H3.
contradiction.
auto.
Qed.

End Finite_sets_facts.