proposition: Lemma partition_inf1 : forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s), Inf x s -> Inf x (fst (partition f s)).
proof: Proof. intros s f x; repeat rewrite <- isok_iff; revert s f x. simple induction s; simpl. - intuition. - intros x l Hrec f a Hs Ha; inv. generalize (Hrec f a H). case (f x); case (partition f l); simpl. + auto. + intros; apply H2; apply Inf_lt with x; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists