From 038d2109e78d9c688acfc3338140cc908151db76 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 5 Apr 2022 12:08:00 +0100 Subject: Generalise 0 comparison to ≤. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda') diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda index ab8a37b..c0207a3 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda @@ -78,6 +78,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 ; x