proposition: Lemma map_union_least {A} (m1 m2 m3 : M A) : m1 ⊆ m3 → m2 ⊆ m3 → m1 ∪ m2 ⊆ m3.
proof: Proof. intros ??. apply map_subseteq_spec. intros ?? [?|[_ ?]]%lookup_union_Some_raw; by eapply lookup_weaken. Qed.
imports: Coq(Permutation) stdpp(options)