proposition: Lemma partition_fst f (m:t elt) : fst (partition f m) = filter f m.
proof: Proof. induction m as [|h l IHl x e r IHr]; simpl; auto. rewrite <- IHl, <-IHr. now destruct (partition f l), (partition f r), f. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)