proposition: Lemma partition_spec1 f m : Proper (K.eq==>eq==>eq) f -> Equal (fst (partition f m)) (filter f m).
proof: Proof. now rewrite partition_alt. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)