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 plus_minus; apply sym_eq; rewrite plus_comm; trivial. Qed.
imports: List more_list list_permut Arith