proposition: Lemma insert_union_singleton_r {A} (m : M A) i x : m !! i = None → <[i:=x]>m = m ∪ {[i := x]}.
proof: Proof. intro. rewrite insert_union_singleton_l, map_union_comm; [done |]. by apply map_disjoint_singleton_l. Qed.
imports: Coq(Permutation) stdpp(options)