proposition: Lemma partition_spec1 : forall s f, @compat_bool elt E.eq f -> Equal (fst (partition f s)) (filter f s).
proof: Proof. intros. rewrite partition_filter. reflexivity. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface