proposition: Lemma partition_spec f m `{!Ok m} : prodmap (@bindings _) (partition f m) = List.partition (fun '(k,e) => f k e) (bindings m).
proof: Proof. rewrite partition_alt, partition_filter. unfold prodmap. f_equal. - now apply filter_spec. - rewrite filter_spec; auto. f_equiv. now intros (k,e) ? <-. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)