diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 542d716f8..21d230e99 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,6 +43,9 @@
   + lemmas `lteD2rE`, `leeD2rE`
   + lemmas `lte_dD2rE`, `lee_dD2rE`
 
+- in `mathcomp_extra.v`:
+  + lemma `invf_ltp`
+
 ### Changed
 
 - in `topology.v`:
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index c4338dd58..77ec6d031 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -63,6 +63,12 @@ Proof.
 by move=> x y ? ?; rewrite -[in LHS](@invrK _ y) ltf_pV2// posrE invr_gt0.
 Qed.
 
+Lemma invf_ltp (F : numFieldType) :
+  {in Num.pos &, forall x y : F, (x < y^-1)%R = (y < x^-1)%R}.
+Proof.
+by move=> x y ? ?; rewrite -[in RHS](@invrK _ y) ltf_pV2// posrE invr_gt0.
+Qed.
+
 Definition proj {I} {T : I -> Type} i (f : forall i, T i) := f i.
 
 Section DFunWith.