proposition: Lemma map_size_delete {A} i (m : M A) : size (delete i m) = (match m !! i with Some _ => pred | None => id end) (size m).
proof: Proof. destruct (m !! i) as [y|] eqn:?; simpl. - by rewrite <-!map_to_list_length, <-(map_to_list_delete m). - by rewrite delete_notin. Qed.
imports: Coq(Permutation) stdpp(options)