proposition: Lemma remove_inf : forall (s : t) (x a : elt) (Hs : Ok s), Inf a s -> Inf a (remove x s).
proof: Proof. induction s; simpl. - intuition. - intros; elim_compare x a; inv; auto. apply Inf_lt with a; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists