proposition: Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
proof: Proof. intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm. rewrite lookup_empty, lookup_union_None in Hm; tauto. Qed.
imports: Coq(Permutation) stdpp(options)