Lemma invf_ltp (#1267)

* Lemma invf_ltp --------- Co-authored-by: Reynald Affeldt <[email protected]>
math-comp · Jul 30, 2024 · fb6dcf0 · fb6dcf0
1 parent 959526d
commit fb6dcf0
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git 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
@@ -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.