proposition: Lemma union_cardinal_inter : forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
proof: Proof. intros. rewrite <- union_inter_cardinal, Nat.add_sub. reflexivity. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide