From e2b91853b58c57b8ad616e728bc55e3570490343 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 5 Apr 2022 13:16:57 +0100
Subject: Add another tiny proof.

---
 .../Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda | 12 ++++++++++++
 src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda |  1 +
 2 files changed, 13 insertions(+)

(limited to 'src/Helium/Algebra/Ordered/StrictTotal')

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
index 4582320..3915f07 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -187,6 +187,18 @@ x⁻¹>1⇒x<1 {x} {x≉0} x⁻¹>1 = ≰⇒>
   ∘ 0≤x<1∧y≤1⇒x*y<1 (<⇒≤ 0<x⁻¹) x⁻¹<1
   )
 
+---- Miscellaneous
+
+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-strict
+  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 9ab34f2..79d3b2d 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -126,6 +126,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
 
   ; -‿⁻¹-comm
   ; x≉0⇒x⁻¹≉0
+  ; y>0∧x<y⇒x*y⁻¹<1
   )
 
 --------------------------------------------------------------------------------
-- 
cgit v1.2.3