proposition: Lemma partition_spec2 : compatb f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
proof: Proof. exact (@M.partition_spec2 _ _). Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts