proposition: Lemma partition_alt1 (f:key->elt->bool) m : fst (partition f m) == filter f m.
proof: Proof. intros k. rewrite !bindings_o. f_equal. replace (bindings (fst _)) with (fst (prodmap (@bindings _) (partition f m))) by now destruct partition. now rewrite partition_spec, filter_spec, partition_filter. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)