proposition: Lemma partition_spec1 : compatb f -> Equal (fst (partition f s)) (filter f s).
proof: Proof. exact (@M.partition_spec1 _ _). Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts