proposition: Lemma union_cardinal_le : forall s s', cardinal (union s s') <= cardinal s + cardinal s'.
proof: Proof. intros; generalize (union_inter_cardinal s s'). intros; rewrite <- H; auto with arith. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide