proposition: Lemma filter_inf : forall (s : t) (x : elt) (f : elt -> bool) (Hs : Ok s), Inf x s -> Inf x (filter f s).
proof: Proof. simple induction s; simpl. - intuition. - intros x l Hrec a f Hs Ha; inv. case (f x); auto. apply Hrec; auto. apply Inf_lt with x; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists