diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 603fd13ac36cc0af945cb9d84c02b5cb742d8ab2..050060069bf61f7e00f4ef72c6b201770b595720 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -715,6 +715,15 @@ Proof.
 Qed.
 
 (** ** Properties of the map operations *)
+Lemma lookup_total_fmap `{!Inhabited A, !Inhabited B} (f : A → B) (m : M A) i :
+  (f <$> m) !!! i =
+    match m !! i with Some _ => f (m !!! i) | None => inhabitant end.
+Proof. rewrite !lookup_total_alt, lookup_fmap. by destruct (m !! i). Qed.
+Lemma lookup_total_fmap' `{!Inhabited A, !Inhabited B}
+    (f : A → B) (m : M A) i :
+  is_Some (m !! i) → (f <$> m) !!! i = f (m !!! i).
+Proof. intros [x Hi]. by rewrite lookup_total_fmap, Hi. Qed.
+
 Global Instance map_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).
 Proof.