diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1692183f0dbb24a4dd0291028618456de8746581..2d5060f6e5564615f9e5b5c70fa76100b46e6bb0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -210,6 +210,7 @@ Pierre Roux, and Thibaut Pérami. Thanks a lot to everyone involved!
   `stdpp.unstable.bitvector_tactics` to `stdpp.bitvector.tactics`. The
   complete library can be imported with `stdpp.bitvector.bitvector`.
   (by Michael Sammler)
+- Add lemma `lookup_total_fmap`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index af749f006febe52203581172daecec546398d45e..655699127f7973727caaeea8aa885b7fe7ba22bb 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -796,6 +796,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.