proposition: Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s.
proof: Proof. unfold Add. split; intros. - red; intros. rewrite H; clear H. fsetdec. - fsetdec. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide