proposition: Lemma delete_notin {A} (m : M A) i : m !! i = None → delete i m = m.
proof: Proof. intros. apply map_eq. intros j. by destruct (decide (i = j)) as [->|?]; rewrite ?lookup_delete, ?lookup_delete_ne. Qed.
imports: Coq(Permutation) stdpp(options)