proposition: Lemma cardinal_union_inter : forall (A B : part_set E) (a b c : nat), cardinal A a -> cardinal B b -> cardinal (inter A B) c -> cardinal (union A B) (a + b - c).
proof: Proof. intros. case (cardinal_diff A H0); intros. case H2; clear H2; intros. case H2; clear H2; intros. case H3; clear H3; intros. apply cardinal_comp with (union A (diff B A)) (a + x); auto with *. rewrite H4. replace c with x0. rewrite plus_assoc. replace (a + x + x0) with (x0 + (a + x)); auto with *. apply (cardinal_unique H3); auto with *. apply cardinal_comp_l with (inter A B); auto with *. Qed.
imports: Fpart Inter Arith