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_filter. rewrite (surjective_pairing (partition f m)). rewrite partition_fst, partition_snd. unfold prodmap. f_equal. - apply filter_spec; auto. - rewrite filter_spec; auto. f_equiv. now intros (k,e) ? <-. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)