diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9dfd0a3f29a591eade0677aea06506e017e02adb..af9fec9786db006d7662977d1bfde4e84999e2f7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -112,6 +112,7 @@ Coq 8.13 is no longer supported.
 * Provide smart constructor `bi_persistently_mixin_discrete` for
   `BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
   property, a trivial definition of the persistence modality can be given.
+* Fix `greatest_fixpoint_ne'` accidentally being about the least fixpoint.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 300a460748407a49e5e5eea3fd407a11e0feb047..f474c5ffb63a8cd94bdf8ddf99a27a65e1185cc0 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -27,7 +27,7 @@ Global Arguments bi_greatest_fixpoint : simpl never.
 
 (* Both non-expansiveness lemmas do not seem to be interderivable.
   FIXME: is there some lemma that subsumes both? *)
-Lemma least_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)):
+Lemma least_fixpoint_ne' {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)):
   (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F).
 Proof. solve_proper. Qed.
 Global Instance least_fixpoint_ne {PROP : bi} {A : ofe} n :
@@ -193,8 +193,8 @@ Qed.
 
 (* Both non-expansiveness lemmas do not seem to be interderivable.
   FIXME: is there some lemma that subsumes both? *)
-Lemma greatest_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)):
-  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F).
+Lemma greatest_fixpoint_ne' {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)):
+  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_greatest_fixpoint F).
 Proof. solve_proper. Qed.
 Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofe} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>