proposition: Lemma union_cardinal: forall s s', (forall x, mem x s && mem x s'=false) -> cardinal (union s s')=cardinal s+cardinal s'.
proof: Proof. intros; apply union_cardinal; auto; intros. rewrite exclusive_set; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx