proposition: Lemma remove_add: mem x s=false -> equal (remove x (add x s)) s=true.
proof: Proof. intros; apply equal_1; apply remove_add; auto. rewrite not_mem_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx