proposition: Lemma exclusive_set : forall s s' x, ~(In x s/\In x s') <-> mem x s && mem x s'=false.
proof: Proof. intros; do 2 rewrite mem_iff. destruct (mem x s); destruct (mem x s'); intuition auto with bool. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx