proposition: Lemma partition_spec A (f:key->A->bool) m : prodmap (@bindings _) (partition f m) = List.partition (fun '(k,e) => f k e) (bindings m).
proof: Proof. unfold partition, prodmap. rewrite partition_filter. f_equiv. apply filter_spec. rewrite filter_spec. f_equiv. now intros (k,e) ? <-. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)