proposition: Lemma add_inf : forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s).
proof: Proof. simple induction s; simpl. - intuition. - intros; elim_compare x a; inv; intuition. Qed.
imports: MSetInterface OrdersFacts OrdersLists