proposition: Lemma cardinal_diff : forall (a : nat) (A B : part_set E), cardinal A a -> exists b : nat, (exists c : nat, cardinal (diff A B) b /\ cardinal (inter A B) c /\ a = b + c).
proof: Proof. simple induction a; intros. exists 0; intros. exists 0; intros. simpl in |- *. split. apply cardinal_empty. apply Trans with (diff (empty E) B); auto with *. split. apply cardinal_empty. apply Trans with (inter (empty E) B); auto with *. auto with *. inversion H0. elim (H B0 B); intros. case H6; clear H6; intros. case H6; clear H6; intros. case H7; clear H7; intros. case (classic (in_part x B)); intros. exists x0. exists (S x1). split. apply cardinal_comp_l with (diff B0 B); auto with *. apply diff_add_part with x; auto with *. split. apply cardinal_add with (inter B0 B) x; auto with *. rewrite H8. auto with *. exists (S x0). exists x1. split. apply cardinal_add with (diff B0 B) x; auto with *. split. apply cardinal_comp_l with (inter B0 B); auto with *. apply inter_add_part_not_in with x; auto with *. rewrite H8; auto with *. auto with *. Qed.
imports: Fpart Inter Arith