proposition: Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) : m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m3 ⊆ m2 ∪ m3 → m1 ⊆ m2.
proof: Proof. intros ??. rewrite !(map_union_comm _ m3) by done. by apply map_union_reflecting_l. Qed.
imports: Coq(Permutation) stdpp(options)