proposition: Lemma partition_iff1 (f:key->elt->bool) : Proper (K.eq==>eq==>eq) f -> forall m k e, MapsTo k e (fst (partition f m)) <-> MapsTo k e m /\ f k e = true.
proof: Proof. intros. rewrite partition_alt1. now apply filter_iff. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)