proposition: Lemma partition_Partition (f:key->elt->bool) : (Proper (K.eq==>eq==>eq) f) -> forall m m1 m2, partition f m = (m1,m2) -> Partition m m1 m2.
proof: Proof. intros Hf m m1 m2 E. replace m1 with (fst (partition f m)) by now rewrite E. replace m2 with (snd (partition f m)) by now rewrite E. clear E. split. - rewrite Disjoint_alt. intros k e e'. rewrite partition_iff1, partition_iff2; auto. intros (U,V) (W,Z). rewrite <- (mapsto_fun U W) in Z; congruence. - intros k e. rewrite partition_iff1, partition_iff2; auto. intuition. destruct (f k e); intuition. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)