proposition: Lemma add_3: forall s x y, x<>y -> In y (add x s) -> In y s.
proof: Proof. intros s x y H. rewrite add_spec. intros [->|?]; trivial. elim H; trivial. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface