proposition: Lemma Partition_Empty m m1 m2 : Partition m m1 m2 -> (Empty m <-> Empty m1 /\ Empty m2).
proof: Proof. intros (Hdisj,Heq). split. intro He. split; intros k e Hke; elim (He k e); rewrite Heq; auto. intros (He1,He2) k e Hke. rewrite Heq in Hke. destruct Hke. elim (He1 k e); auto. elim (He2 k e); auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)