Lemma invf_ltp

math-comp · Jul 24, 2024 · b49b983 · b49b983
1 parent 85a2a3b
commit b49b983
Showing 1 changed file with 6 additions and 0 deletions.
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.