proposition: Lemma lookup_delete_None {A} (m : M A) i j : delete i m !! j = None ↔ i = j ∨ m !! j = None.
proof: Proof. destruct (decide (i = j)) as [->|?]; rewrite ?lookup_delete, ?lookup_delete_ne; tauto. Qed.
imports: Coq(Permutation) stdpp(options)