proposition: Lemma cardinal_union_lemma A B : # (A ∪ B) = # A + # B - # (A ∩ B).
proof: Proof. cut (# (A ∪ B) + # (A ∩ B) = # A + # B). lia. unfold cardinal. repeat rewrite <-Nat2Z.inj_add. f_equal. unfold binary_intersection, binary_union in *. induction enum_X as [| x l IHl]. reflexivity. simpl. destruct (A x), (B x); simpl; repeat rewrite <-plus_n_Sm; congruence. Qed.
imports: Lists.List ZArith Setoid Coq.Classes.Morphisms Lia