proposition: Lemma add_cardinal_2: forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
proof: Proof. intros; apply add_cardinal_2; auto. rewrite not_mem_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx