proposition: Lemma remove_spec: forall s x y, In y (remove x s) <-> In y s /\ y<>x.
proof: Proof. unfold In. intros s x y; revert x y s. induction x; intros [y|y|] [|l o r]; simpl remove; rewrite ?mem_node; simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface