proposition: Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 -> let f := fun k (_:elt) => mem k m1 in Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)).
proof: Proof. intros m m1 m2 Hm f. assert (Hf : Proper (E.eq==>eq==>eq) f). { intros k k' Hk e e' _; unfold f; rewrite Hk; auto. } set (m1':= fst (partition f m)). set (m2':= snd (partition f m)). split; rewrite Equal_mapsto_iff; intros k e. - rewrite (@partition_iff_1 f Hf m m1') by auto. unfold f. rewrite <- mem_in_iff. destruct Hm as (Hm,Hm'). rewrite Hm'. intuition. + exists e; auto. + elim (Hm k); split; auto; exists e; auto. - rewrite (@partition_iff_2 f Hf m m2') by auto. unfold f. rewrite <- not_mem_in_iff. destruct Hm as (Hm,Hm'). rewrite Hm'. intuition. + elim (Hm k); split; auto; exists e; auto. + elim H1; exists e; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface