proposition: Lemma Partition_Empty : forall m m1 m2, Partition m m1 m2 -> (Empty m <-> (Empty m1 /\ Empty m2)).
proof: Proof. intros m m1 m2 (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: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface