proposition: Lemma add_spec : forall (s : t) (x y : elt) (Hs : Ok s), In y (add x s) <-> X.eq y x \/ In y s.
proof: Proof. induction s; simpl; intros. - intuition. inv; auto. - elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition. Qed.
imports: MSetInterface OrdersFacts OrdersLists