proposition: Lemma partition_Partition : forall m m1 m2, partition f m = (m1,m2) -> Partition m m1 m2.
proof: Proof. intros. split. - rewrite Disjoint_alt. intros k e e'. rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) by (rewrite H; auto). intros (U,V) (W,Z). rewrite <- (MapsTo_fun U W) in Z; congruence. - intros k e. rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) by (rewrite H; auto). destruct (f k e); intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface