proposition: Lemma partition_iff2 (f:key->elt->bool) : Proper (K.eq==>eq==>eq) f -> forall m k e, MapsTo k e (snd (partition f m)) <-> MapsTo k e m /\ f k e = false.
proof: Proof. intros. rewrite partition_alt2. rewrite filter_iff. now rewrite negb_true_iff. clear -H. intros x x' Hx e e' <-. f_equal. now apply H. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)