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