proposition: Lemma Partition_sym : forall m m1 m2, Partition m m1 m2 -> Partition m m2 m1.
proof: Proof. intros m m1 m2 (H,H'); split. - apply Disjoint_sym; auto. - intros; rewrite H'; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface