proposition: Lemma Partition_partition m m1 m2 : Partition m m1 m2 -> let f := fun k _ => mem k m1 in m1 == fst (partition f m) /\ m2 == snd (partition f m).
proof: Proof. intros Hm f. assert (Hf : Proper (K.eq==>eq==>eq) f). { intros k k' Hk e e' _; unfold f; rewrite Hk; auto. } split; rewrite Equal_mapsto_iff; intros k e. - rewrite partition_iff1; auto. unfold f. rewrite <- mem_in_iff. destruct Hm as (Hm,->). firstorder. - rewrite partition_iff2; auto. unfold f. rewrite <- not_mem_in_iff. destruct Hm as (Hm,->). firstorder. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)