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