proposition: Lemma lookup_delete_Some {A} (m : M A) i j y : delete i m !! j = Some y ↔ i ≠ j ∧ m !! j = Some y.
proof: Proof. split. - destruct (decide (i = j)) as [->|?]; rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence. - intros [??]. by rewrite lookup_delete_ne. Qed.
imports: Coq(Permutation) stdpp(options)