proposition: Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y.
proof: Proof. split; [split; [apply remove_3 with x |] | destruct 1; apply remove_2]; auto. intro. apply (remove_1 H0 H). Qed.
imports: DecidableTypeEx FSetInterface