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