proposition: Lemma cardinal_union_disjoint : forall (a b : nat) (A B : part_set E), cardinal A a -> cardinal B b -> disjoint A B -> cardinal (union A B) (a + b).
proof: Proof. simple induction a. intros. apply cardinal_comp_l with (union (empty E) B); auto with *. apply union_comp; auto with *. apply Sym. auto with *. apply cardinal_comp_l with B; auto with *. intros. inversion H0. simpl in |- *. apply cardinal_add with (union B0 B) x; auto with *. apply H; auto with *. apply disjoint_inclus with (add_part B0 x); auto with *. apply disjoint_comp with A B; auto with *. apply union_not_in; auto with *. apply disjoint_not_in_r with A; auto with *. apply in_part_comp_r with (add_part B0 x); auto with *. apply Trans with (union (add_part B0 x) B); auto with *. unfold add_part in |- *. apply Trans with (union B0 (union (single x) B)); auto with *. apply Trans with (union B0 (union B (single x))); auto with *. Qed.
imports: Fpart Inter Arith