proposition: Lemma cardinal_binary_union A B : cardinal (binary_union A B) = cardinal A + cardinal B - cardinal (binary_intersection A B).
proof: Proof. rewrite <-cardinal_union_lemma. lia. Qed.
imports: Lists.List ZArith Setoid Coq.Classes.Morphisms Lia