proposition: Lemma Partition_sym m m1 m2 : Partition m m1 m2 -> Partition m m2 m1.
proof: Proof. intros (H,H'); split. apply Disjoint_sym; auto. intros; rewrite H'; intuition. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)