proposition: Lemma remove_cardinal_2: forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
proof: Proof. intros; apply Equal_cardinal; apply equal_2; auto with set. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx