proposition: Lemma delete_commute {A} (m : M A) i j : delete i (delete j m) = delete j (delete i m).
proof: Proof. destruct (decide (i = j)) as [->|]; [done|]. by apply partial_alter_commute. Qed.
imports: Coq(Permutation) stdpp(options)