proposition: Lemma cardinal_union: forall s1 s2, cardinal (union s1 s2) = cardinal s1 + cardinal s2 - cardinal (inter s1 s2).
proof: Proof. intros s1 s2; assert (H := cardinal_union_inter_12 s1 s2). apply sym_eq, Nat.add_sub_eq_r; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)