proposition: Lemma cardinal_union : forall (a b : nat) (A B : part_set E), cardinal A a -> cardinal (diff B A) b -> cardinal (union A B) (a + b).
proof: Proof. intros. apply cardinal_comp_l with (union A (diff B A)); auto with *. Qed.
imports: Fpart Inter Arith