2 files changed, 11 insertions, 1 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
index 3915f07..4469c03 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -199,6 +199,16 @@ y>0∧x<y⇒x*y⁻¹<1 {x} {y} y>0 x<y = x≥0⇒*-cancelʳ-< (<⇒≤ y>0) (beg
   1# * y           ∎)
   where y≉0 = <⇒≉ y>0 ∘ Eq.sym
 
+y>0∧x≤y⇒x*y⁻¹≤1 : ∀ {x y} (y>0 : y > 0#) → x ≤ y → x * (<⇒≉ y>0 ∘ Eq.sym) ⁻¹ ≤ 1#
+y>0∧x≤y⇒x*y⁻¹≤1 {x} {y} y>0 x≤y = x>0⇒*-cancelʳ-≤ y>0 (begin
+  x * y≉0 ⁻¹ * y   ≈⟨  *-assoc x _ y ⟩
+  x * (y≉0 ⁻¹ * y) ≈⟨  *-congˡ (⁻¹-inverseˡ y≉0) ⟩
+  x * 1#           ≈⟨  *-identityʳ x ⟩
+  x                ≤⟨  x≤y ⟩
+  y                ≈˘⟨ *-identityˡ y ⟩
+  1# * y           ∎)
+  where y≉0 = <⇒≉ y>0 ∘ Eq.sym
+
 --------------------------------------------------------------------------------
 ---- Properties of -_ and _⁻¹
 
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
index 79d3b2d..eb46e27 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -126,7 +126,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
 
   ; -‿⁻¹-comm
   ; x≉0⇒x⁻¹≉0
-  ; y>0∧x<y⇒x*y⁻¹<1
+  ; y>0∧x<y⇒x*y⁻¹<1; y>0∧x≤y⇒x*y⁻¹≤1
   )
 
 --------------------------------------------------------------------------------