From 2866b11be6eebc4fcb37bbbc8851b44fafdd0c19 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Sun, 13 Jan 2019 12:05:30 +0000
Subject: [PATCH] Total order on the rationals (#17)

---
 Fields/FieldOfFractions.agda      |  38 +--
 Fields/FieldOfFractionsOrder.agda | 425 ++++++++++++++++++++++++++++++
 Fields/Fields.agda                |  44 ++++
 Groups/GroupDefinition.agda       |  22 ++
 Groups/Groups.agda                |  20 +-
 Groups/GroupsLemmas.agda          |   1 +
 Rings/IntegralDomains.agda        |   1 +
 Rings/RingDefinition.agda         |   1 +
 Rings/RingLemmas.agda             | 124 +++++++++
 9 files changed, 624 insertions(+), 52 deletions(-)
 create mode 100644 Fields/FieldOfFractionsOrder.agda
 create mode 100644 Groups/GroupDefinition.agda

diff --git a/Fields/FieldOfFractions.agda b/Fields/FieldOfFractions.agda
index 677ab45..a32c425 100644
--- a/Fields/FieldOfFractions.agda
+++ b/Fields/FieldOfFractions.agda
@@ -2,6 +2,7 @@
 
 open import LogicalFormulae
 open import Groups.Groups
+open import Groups.GroupDefinition
 open import Groups.GroupsLemmas
 open import Rings.RingDefinition
 open import Rings.RingLemmas
@@ -9,7 +10,6 @@ open import Rings.IntegralDomains
 open import Fields.Fields
 open import Functions
 open import Setoids.Setoids
-open import Setoids.Orders
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
@@ -229,39 +229,3 @@ module Fields.FieldOfFractions where
       open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
       open Transitive (Equivalence.transitiveEq (Setoid.eq S))
       open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
-
-  fieldOfFractionsNonnegDenom : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → (a1 : fieldOfFractionsSet I) → Sg (fieldOfFractionsSet I) (λ b1 → (Setoid._∼_ (fieldOfFractionsSetoid I) a1 b1) && ((Ring.0R R) < underlying (_&&_.snd b1)))
-  fieldOfFractionsNonnegDenom {R = R} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) denom
-  fieldOfFractionsNonnegDenom {R = R} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) | inl (inl 0<denom) = (num ,, (denom , denom!=0)) , ((Ring.multCommutative R) ,, 0<denom)
-  fieldOfFractionsNonnegDenom {S = S} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) | inl (inr denom<0) = ((Group.inverse (Ring.additiveGroup R) num ,, (Group.inverse (Ring.additiveGroup R) denom , λ p → denom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (transitive (symmetric (Group.invLeft (Ring.additiveGroup R) {denom})) (transitive (Group.wellDefined (Ring.additiveGroup R) p reflexive) (Group.multIdentLeft (Ring.additiveGroup R)))))))) , (transitive (ringMinusExtracts R) (transitive (inverseWellDefined (Ring.additiveGroup R) (Ring.multCommutative R)) (symmetric (ringMinusExtracts R))) ,, ringMinusFlipsOrder' order (SetoidPartialOrder.wellDefined pOrder (symmetric (invInv (Ring.additiveGroup R))) reflexive denom<0))
-    where
-      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
-      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
-      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
-      open Ring R
-      open Group additiveGroup
-  fieldOfFractionsNonnegDenom {S = S} {R = R} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) | inr 0=denom = exFalso (denom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denom))
-
-  fieldOfFractionsComparison : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → Rel (fieldOfFractionsSet I)
-  fieldOfFractionsComparison {_*_ = _*_} {R = R} {_<_ = _<_} {tOrder = tOrder} I oring x y with fieldOfFractionsNonnegDenom I oring x
-  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} I oring x y | (numA ,, (denomA , _)) , b with fieldOfFractionsNonnegDenom I oring y
-  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} I oring x y | (numA ,, (denomA , _)) , prA | (numB ,, (denomB , _)) , prB = (numA * denomB) < (numB * denomA)
-
-  fieldOfFractionsOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidPartialOrder (fieldOfFractionsSetoid I) (fieldOfFractionsComparison I order)
-  SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_ = _+_} {_*_ = _*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c with fieldOfFractionsNonnegDenom I order x
-  SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) with fieldOfFractionsNonnegDenom I order z
-  SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) | (numZ ,, (denomZ , denomZ!=0)) , (numZ/denomZ ,, 0<denomZ) with fieldOfFractionsNonnegDenom I order w
-  SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) | (numZ ,, (denomZ , denomZ!=0)) , (numZ/denomZ ,, 0<denomZ) | (numW ,, (denomW , denomW!=0)) , (numW/denomW ,, 0<denomW) with fieldOfFractionsNonnegDenom I order y
-  SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {numW' ,, (denomW' , denomW'!=0)} {numX' ,, (denomX' , denomX'!=0)} {numY' ,, (denomY' , denomY'!=0)} {numZ' ,, (denomZ' , denomZ'!=0)} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) | (numZ ,, (denomZ , denomZ!=0)) , (numZ/denomZ ,, 0<denomZ) | (numW ,, (denomW , denomW!=0)) , (numW/denomW ,, 0<denomW) | (numY ,, (denomY , denomY!=0)) , (numY/denomY ,, 0<denomY) = {!!}
-
-  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder = tOrder} I oRing) {x} x<x with fieldOfFractionsNonnegDenom I oRing x
-  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {x} x<x | (numA ,, (denomA , _)) , pr with fieldOfFractionsNonnegDenom I oRing x
-  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {fst₁ ,, (a , a!=0)} x<x | (numA ,, (denomA , _)) , (fst₂ ,, 0<denomA) | (numA' ,, (denomA' , _)) , (fst ,, 0<denomA') = {!!}
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order) {numA ,, (denomA , _)} {(numB ,, (denomB , _))} {numC ,, (denomC , _)} a<b b<c = {!!}
-
-  fieldOfFractionsTotalOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidTotalOrder (fieldOfFractionsOrder I order)
-  fieldOfFractionsTotalOrder I order = {!!}
-
-  fieldOfFractionsOrderedRing : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → OrderedRing (fieldOfFractionsRing I) (fieldOfFractionsTotalOrder I order)
-  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing I order) a<b c = {!!}
-  OrderedRing.orderRespectsMultiplication (fieldOfFractionsOrderedRing {_+_ = _+_} {_*_ = _*_} {_<_ = _<_} I order) {numA ,, (denomA , _)} {numB ,, (denomB , _)} 0<a 0<b = {!!}
diff --git a/Fields/FieldOfFractionsOrder.agda b/Fields/FieldOfFractionsOrder.agda
new file mode 100644
index 0000000..464a273
--- /dev/null
+++ b/Fields/FieldOfFractionsOrder.agda
@@ -0,0 +1,425 @@
+{-# OPTIONS --safe --warning=error #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.GroupDefinition
+open import Groups.GroupsLemmas
+open import Rings.RingDefinition
+open import Rings.RingLemmas
+open import Rings.IntegralDomains
+open import Fields.Fields
+open import Functions
+open import Setoids.Setoids
+open import Setoids.Orders
+open import Fields.FieldOfFractions
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Fields.FieldOfFractionsOrder where
+
+  fieldOfFractionsComparison : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → Rel (fieldOfFractionsSet I)
+  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) = (numA * denomB) < (numB * denomA)
+  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) = (numB * denomA) < (numA * denomB)
+  fieldOfFractionsComparison {S = S} {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
+    where
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) = (numB * denomA) < (numA * denomB)
+  fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) = (numA * denomB) < (numB * denomA)
+  fieldOfFractionsComparison {S = S} {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
+    where
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  fieldOfFractionsComparison {S = S} {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inr 0=denomA = exFalso (denomA!=0 (symmetric 0=denomA))
+    where
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+
+  fieldOfFractionsOrderWellDefinedLeft : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → {x y z : fieldOfFractionsSet I} → fieldOfFractionsComparison I order x y → Setoid._∼_ (fieldOfFractionsSetoid I) x z → fieldOfFractionsComparison I order z y
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R = R} {tOrder = tOrder} I order {(numX ,, (denomX , denomX!=0))} {(numY ,, (denomY , denomY!=0))} {(numZ ,, (denomZ , denomZ!=0))} x<y x=z with SetoidTotalOrder.totality tOrder (Ring.0R R) denomZ
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inl _) = s
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      have : ((numX * denomY) * denomZ) < ((numY * denomX) * denomZ)
+      have = ringCanMultiplyByPositive order 0<denomZ x<y
+      p : ((numX * denomZ) * denomY) < ((numY * denomX) * denomZ)
+      p = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) reflexive have
+      q : ((denomX * numZ) * denomY) < ((numY * denomX) * denomZ)
+      q = SetoidPartialOrder.wellDefined pOrder (multWellDefined x=z reflexive) reflexive p
+      r : ((numZ * denomY) * denomX) < ((numY * denomZ) * denomX)
+      r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) multCommutative) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) q
+      s : (numZ * denomY) < (numY * denomZ)
+      s = ringCanCancelPositive order 0<denomX r
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inr x) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (symmetric x))
+    where
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inl _) = ringCanCancelNegative order denomX<0 r
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      p : ((numY * denomX) * denomZ) < ((numX * denomZ) * denomY)
+      p = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive order 0<denomZ x<y)
+      q : ((numY * denomX) * denomZ) < ((denomX * numZ) * denomY)
+      q = SetoidPartialOrder.wellDefined pOrder reflexive (multWellDefined x=z reflexive) p
+      r : ((numY * denomZ) * denomX) < ((numZ * denomY) * denomX)
+      r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) multCommutative) q
+
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inr x) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inr 0=denomX = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomX))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inr _) = ringCanCancelPositive order 0<denomX r
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      p : ((numY * denomX) * denomZ) < ((numX * denomY) * denomZ)
+      p = ringCanMultiplyByPositive order 0<denomZ x<y
+      q : ((numY * denomX) * denomZ) < ((denomX * numZ) * denomY)
+      q = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (multWellDefined x=z reflexive)))) p
+      r : ((numY * denomZ) * denomX) < ((numZ * denomY) * denomX)
+      r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) multCommutative) q
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inr _) = ringCanCancelNegative order denomX<0 q
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      p : ((numX * denomY) * denomZ) < ((numY * denomX) * denomZ)
+      p = ringCanMultiplyByPositive order 0<denomZ x<y
+      q : ((numZ * denomY) * denomX) < ((numY * denomZ) * denomX)
+      q = SetoidPartialOrder.wellDefined pOrder (transitive (multWellDefined multCommutative reflexive) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive multCommutative (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) p
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inr 0=denomX = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomX))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inr 0=denomY = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomY))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inl _) = ringCanCancelPositive order 0<denomX (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive (multWellDefined reflexive (multCommutative)) (transitive multAssoc (multWellDefined multCommutative reflexive))))) p)
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      p : ((numY * denomX) * denomZ) < ((denomY * numX) * denomZ)
+      p = ringCanMultiplyByNegative order denomZ<0 (SetoidPartialOrder.wellDefined pOrder multCommutative reflexive x<y)
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inr denomY<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inl _) = ringCanCancelNegative order denomX<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined x=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) p)
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      p : ((numX * denomY) * denomZ) < ((numY * denomX) * denomZ)
+      p = ringCanMultiplyByNegative order denomZ<0 x<y
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inr denomY<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder denomY<0 0<denomY))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) | inr 0=denomY = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomY))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inr x = exFalso (denomX!=0 (symmetric x))
+    where
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inr _) = ringCanCancelPositive order 0<denomX (SetoidPartialOrder.wellDefined pOrder (transitive (multWellDefined multCommutative reflexive) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive multAssoc (transitive multCommutative multAssoc))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByNegative order denomZ<0 x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inr _) = ringCanCancelNegative order denomX<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (multWellDefined multCommutative reflexive) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (multWellDefined multCommutative reflexive)))))) (ringCanMultiplyByNegative order denomZ<0 x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inr x = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inr x = exFalso (denomY!=0 (symmetric x))
+    where
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inr 0=denomZ = exFalso (denomZ!=0 (symmetric 0=denomZ))
+    where
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+
+  fieldOfFractionsOrderWellDefinedRight : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → {x y z : fieldOfFractionsSet I} → fieldOfFractionsComparison I order x y → Setoid._∼_ (fieldOfFractionsSetoid I) y z → fieldOfFractionsComparison I order x z
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R = R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomZ
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByPositive order 0<denomZ x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive order 0<denomZ x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByNegative order denomZ<0 x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive (multAssoc) (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByNegative order denomZ<0 x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inr x = exFalso (denomZ!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomZ
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive order 0<denomZ x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByPositive order 0<denomZ x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByNegative order denomZ<0 x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByNegative order denomZ<0 x<y))
+    where
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inr x = exFalso (denomZ!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inr x = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+
+  swapLemma : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+_ _*_) {x y z : A} → Setoid._∼_ S ((x * y) * z) ((x * z) * y)
+  swapLemma {S = S} R = transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+
+  fieldOfFractionsOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidPartialOrder (fieldOfFractionsSetoid I) (fieldOfFractionsComparison I order)
+  SetoidPartialOrder.wellDefined (fieldOfFractionsOrder I oRing) {a} {b} {c} {d} a=b c=d a<c = fieldOfFractionsOrderWellDefinedRight I oRing {b} {c} {d} (fieldOfFractionsOrderWellDefinedLeft I oRing {a} {c} {b} a<c a=b) c=d
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder = tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr with SetoidTotalOrder.totality tOrder (Ring.0R R) aDenom
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) with SetoidTotalOrder.totality tOrder (Ring.0R R) aDenom
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inl (inl _) = SetoidPartialOrder.irreflexive pOrder pr
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inl (inr aDenom<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<aDenom aDenom<0))
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inr x = exFalso (aDenom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) aDenom
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inl (inl 0<aDenom) = SetoidPartialOrder.irreflexive pOrder pr
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inl (inr _) = SetoidPartialOrder.irreflexive pOrder pr
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inr x = exFalso (aDenom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inr x = exFalso (aDenom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder = tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl x) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inl _) = ringCanCancelPositive oRing 0<denomB p
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      inter : ((numA * denomB) * denomC) < ((numB * denomA) * denomC)
+      inter = ringCanMultiplyByPositive oRing 0<denomC a<b
+      p : ((numA * denomC) * denomB) < ((numC * denomA) * denomB)
+      p = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) reflexive inter) (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive oRing 0<denomA b<c))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inl _) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) reflexive (ringCanMultiplyByPositive oRing 0<denomA b<c)) (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive oRing 0<denomC a<b)))
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inl 0<denomC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inr _) = ringCanCancelPositive oRing 0<denomB (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomC<0 a<b)))
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      have : ((numC * denomA) * denomB) < ((numB * denomC)  * denomA)
+      have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByPositive oRing 0<denomA b<c)
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  ... | (inl (inl 0<denomC)) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  ... | (inl (inr _)) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByPositive oRing 0<denomA b<c)))
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
+      have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByNegative oRing denomC<0 a<b)
+  ... | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inl _) = ringCanCancelPositive oRing 0<denomB (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)) have)
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      have : ((numB * denomA) * denomC) < ((numA * denomC) * denomB)
+      have = SetoidPartialOrder.wellDefined pOrder reflexive (swapLemma R) (ringCanMultiplyByPositive oRing 0<denomC a<b)
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inl _) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)))
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
+      have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByPositive oRing 0<denomC a<b)
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inl 0<denomC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inr _) = ringCanCancelPositive oRing 0<denomB (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)))
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
+      have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByNegative oRing denomC<0 a<b)
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) | inl (inl 0<denomC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) | inl (inr _) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)) have)
+    where
+      open Setoid S
+      open Ring R
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      have : ((numB * denomA) * denomC) < ((numA * denomC) * denomB)
+      have = SetoidPartialOrder.wellDefined pOrder reflexive (swapLemma R) (ringCanMultiplyByNegative oRing denomC<0 a<b)
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+
+  fieldOfFractionsTotalOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidTotalOrder (fieldOfFractionsOrder I order)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) with SetoidTotalOrder.totality tOrder (numA * denomB) (numB * denomA)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) | inl (inl x) = inl (inl x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) | inl (inr x) = inl (inr x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) | inr x = inr (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) x (Ring.multCommutative R))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inr denomA<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) with SetoidTotalOrder.totality tOrder (numB * denomA) (numA * denomB)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) | inl (inl x) = inl (inl x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) | inl (inr x) = inl (inr x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) | inr x = inr (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) (Ring.multCommutative R) x))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inr denomA<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inl 0<denomA) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) with SetoidTotalOrder.totality tOrder (numB * denomA) (numA * denomB)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) | inl (inl x) = inl (inl x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) | inl (inr x) = inl (inr x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) | inr x = inr (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x) (Ring.multCommutative R))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inl 0<denomA) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) with SetoidTotalOrder.totality tOrder (numA * denomB) (numB * denomA)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) | inl (inl x) = inl (inl x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) | inl (inr x) = inl (inr x)
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) | inr x = inr (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) x (Ring.multCommutative R))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+
+{-
+  fieldOfFractionsOrderedRing : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → OrderedRing (fieldOfFractionsRing I) (fieldOfFractionsTotalOrder I order)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) (denomA * denomC)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) with SetoidTotalOrder.totality tOrder (Ring.0R R) (denomB * denomC)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) | inl (inl 0<dB) = {!!}
+    where
+      open Ring R
+      0<dC : 0R < denomC
+      0<dC with SetoidTotalOrder.totality tOrder 0R denomC
+      0<dC | inl (inl x) = x
+      0<dC | inl (inr dC<0) = {!!}
+      0<dC | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) | inl (inr dB<0) = {!!}
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inr dA<0) = {!!}
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inr dBdC<0) = {!!}
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inr 0=dBdC with IntegralDomain.intDom I (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=dBdC)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inr 0=dBdC | inl x = exFalso (denomB!=0 x)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inr 0=dBdC | inr x = exFalso (denomC!=0 x)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) = {!!}
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inr (0=dAdC) with IntegralDomain.intDom I (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=dAdC)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inr 0=dAdC | inl x = exFalso (denomA!=0 x)
+  OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inr 0=dAdC | inr x = exFalso (denomC!=0 x)
+  OrderedRing.orderRespectsMultiplication (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) = {!!}
+
+-}
diff --git a/Fields/Fields.agda b/Fields/Fields.agda
index 7f54927..e61db5e 100644
--- a/Fields/Fields.agda
+++ b/Fields/Fields.agda
@@ -2,8 +2,11 @@
 
 open import LogicalFormulae
 open import Groups.Groups
+open import Groups.GroupDefinition
 open import Rings.RingDefinition
+open import Rings.RingLemmas
 open import Setoids.Setoids
+open import Setoids.Orders
 open import Orders
 open import Rings.IntegralDomains
 open import Functions
@@ -19,6 +22,47 @@ module Fields.Fields where
       allInvertible : (a : A) → ((a ∼ Group.identity (Ring.additiveGroup R)) → False) → Sg A (λ t → t * a ∼ 1R)
       nontrivial : (0R ∼ 1R) → False
 
+  orderedFieldIsIntDom : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {c} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (O : OrderedRing R tOrder) (F : Field R) → IntegralDomain R
+  IntegralDomain.intDom (orderedFieldIsIntDom {S = S} {_*_ = _*_} {R = R} {tOrder = tOrder} O F) {a} {b} ab=0 with SetoidTotalOrder.totality tOrder (Ring.0R R) a
+  IntegralDomain.intDom (orderedFieldIsIntDom {A = A} {S = S} {_*_ = _*_} {R = R} {pOrder = pOrder} {tOrder = tOrder} O F) {a} {b} ab=0 | inl (inl x) = inr (transitive (transitive (symmetric multIdentIsIdent) (multWellDefined q reflexive)) p')
+    where
+      open Setoid S
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      open Ring R
+      a!=0 : (a ∼ Group.identity additiveGroup) → False
+      a!=0 pr = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder (symmetric pr) reflexive x)
+      invA : A
+      invA = underlying (Field.allInvertible F a a!=0)
+      q : 1R ∼ (invA * a)
+      q with Field.allInvertible F a a!=0
+      ... | invA , pr = symmetric pr
+      p : invA * (a * b) ∼ invA * Group.identity additiveGroup
+      p = multWellDefined reflexive ab=0
+      p' : (invA * a) * b ∼ Group.identity additiveGroup
+      p' = transitive (symmetric multAssoc) (transitive p (ringTimesZero R))
+  IntegralDomain.intDom (orderedFieldIsIntDom {A = A} {S = S} {_*_ = _*_} {R = R} {pOrder = pOrder} {tOrder = tOrder} O F) {a} {b} ab=0 | inl (inr x) = inr (transitive (transitive (symmetric multIdentIsIdent) (multWellDefined q reflexive)) p')
+    where
+      open Setoid S
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      open Ring R
+      a!=0 : (a ∼ Group.identity additiveGroup) → False
+      a!=0 pr = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder reflexive (symmetric pr) x)
+      invA : A
+      invA = underlying (Field.allInvertible F a a!=0)
+      q : 1R ∼ (invA * a)
+      q with Field.allInvertible F a a!=0
+      ... | invA , pr = symmetric pr
+      p : invA * (a * b) ∼ invA * Group.identity additiveGroup
+      p = multWellDefined reflexive ab=0
+      p' : (invA * a) * b ∼ Group.identity additiveGroup
+      p' = transitive (symmetric multAssoc) (transitive p (ringTimesZero R))
+  IntegralDomain.intDom (orderedFieldIsIntDom {S = S} {_*_ = _*_} {R = R} {tOrder = tOrder} O F) {a} {b} ab=0 | inr x = inl (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x)
+  IntegralDomain.nontrivial (orderedFieldIsIntDom {S = S} O F) pr = Field.nontrivial F (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) pr)
+
   record Field' {m n : _} : Set (lsuc m ⊔ lsuc n) where
     field
       A : Set m
diff --git a/Groups/GroupDefinition.agda b/Groups/GroupDefinition.agda
new file mode 100644
index 0000000..d86f0d8
--- /dev/null
+++ b/Groups/GroupDefinition.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --safe --warning=error #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Functions
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Numbers.Naturals
+open import Sets.FinSet
+
+module Groups.GroupDefinition where
+
+  record Group {lvl1 lvl2} {A : Set lvl1} (S : Setoid {lvl1} {lvl2} A) (_·_ : A → A → A) : Set (lsuc lvl1 ⊔ lvl2) where
+    open Setoid S
+    field
+      wellDefined : {m n x y : A} → (m ∼ x) → (n ∼ y) → (m · n) ∼ (x · y)
+      identity : A
+      inverse : A → A
+      multAssoc : {a b c : A} → (a · (b · c)) ∼ (a · b) · c
+      multIdentRight : {a : A} → (a · identity) ∼ a
+      multIdentLeft : {a : A} → (identity · a) ∼ a
+      invLeft : {a : A} → (inverse a) · a ∼ identity
+      invRight : {a : A} → a · (inverse a) ∼ identity
diff --git a/Groups/Groups.agda b/Groups/Groups.agda
index 7d6a3a5..c28ea6f 100644
--- a/Groups/Groups.agda
+++ b/Groups/Groups.agda
@@ -6,19 +6,9 @@ open import Functions
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Numbers.Naturals
 open import Sets.FinSet
+open import Groups.GroupDefinition
 
 module Groups.Groups where
-    record Group {lvl1 lvl2} {A : Set lvl1} (S : Setoid {lvl1} {lvl2} A) (_·_ : A → A → A) : Set (lsuc lvl1 ⊔ lvl2) where
-      open Setoid S
-      field
-        wellDefined : {m n x y : A} → (m ∼ x) → (n ∼ y) → (m · n) ∼ (x · y)
-        identity : A
-        inverse : A → A
-        multAssoc : {a b c : A} → (a · (b · c)) ∼ (a · b) · c
-        multIdentRight : {a : A} → (a · identity) ∼ a
-        multIdentLeft : {a : A} → (identity · a) ∼ a
-        invLeft : {a : A} → (inverse a) · a ∼ identity
-        invRight : {a : A} → a · (inverse a) ∼ identity
 
     reflGroupWellDefined : {lvl : _} {A : Set lvl} {m n x y : A} {op : A → A → A} → m ≡ x → n ≡ y → (op m n) ≡ (op x y)
     reflGroupWellDefined {lvl} {A} {m} {n} {.m} {.n} {op} refl refl = refl
@@ -185,8 +175,8 @@ module Groups.Groups where
         open Transitive transitiveEq
         open Symmetric symmetricEq
 
-    invContravariant : {a b : _} → {A : Set a} → {S : Setoid {a} {b} A} → {_·_ : A → A → A} → (G : Group S _·_) → (x y : A) → (Setoid._∼_ S (Group.inverse G (x · y)) ((Group.inverse G y) · (Group.inverse G x)))
-    invContravariant {S = S} {_·_} G x y = ans
+    invContravariant : {a b : _} → {A : Set a} → {S : Setoid {a} {b} A} → {_·_ : A → A → A} → (G : Group S _·_) → {x y : A} → (Setoid._∼_ S (Group.inverse G (x · y)) ((Group.inverse G y) · (Group.inverse G x)))
+    invContravariant {S = S} {_·_} G {x} {y} = ans
       where
         open Group G renaming (inverse to _^-1) renaming (identity to e)
         open Setoid S
@@ -361,7 +351,7 @@ module Groups.Groups where
             g : f (Group.inverse G (m ·A Group.inverse G n)) ∼ identity
             g = transitive (homRespectsInverse fHom {m ·A Group.inverse G n}) (transitive (inverseWellDefined H pr) (invIdentity H))
             h : f (Group.inverse G (Group.inverse G n) ·A Group.inverse G m) ∼ identity
-            h = transitive (GroupHom.wellDefined fHom (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (invContravariant G m (Group.inverse G n)))) g
+            h = transitive (GroupHom.wellDefined fHom (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (invContravariant G))) g
             i : f (n ·A Group.inverse G m) ∼ identity
             i = transitive (GroupHom.wellDefined fHom (Group.wellDefined G (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (invTwice G n)) (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))))) h
         Transitive.transitive (Equivalence.transitiveEq (Setoid.eq ansSetoid)) {m} {n} {o} prmn prno = transitive (GroupHom.wellDefined fHom (Group.wellDefined G (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (Group.multIdentLeft G)))) k
@@ -392,7 +382,7 @@ module Groups.Groups where
         p6 : (f x) ·B (Group.identity H ·B f (Group.inverse G m)) ∼ (f x) ·B f (Group.inverse G m)
         p7 : (f x) ·B f (Group.inverse G m) ∼ f (x ·A (Group.inverse G m))
         p8 : f (x ·A (Group.inverse G m)) ∼ Group.identity H
-        p1 = GroupHom.wellDefined fHom (Group.wellDefined G (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (invContravariant G m n))
+        p1 = GroupHom.wellDefined fHom (Group.wellDefined G (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (invContravariant G))
         p2 = GroupHom.wellDefined fHom (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (fourWayAssoc G))
         p3 = GroupHom.groupHom fHom
         p4 = Group.wellDefined H (Reflexive.reflexive reflexiveEq) (GroupHom.groupHom fHom)
diff --git a/Groups/GroupsLemmas.agda b/Groups/GroupsLemmas.agda
index d2b6e04..15a2504 100644
--- a/Groups/GroupsLemmas.agda
+++ b/Groups/GroupsLemmas.agda
@@ -6,6 +6,7 @@ open import Functions
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Numbers.Naturals
 open import Groups.Groups
+open import Groups.GroupDefinition
 
 module Groups.GroupsLemmas where
   invInv : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → Setoid._∼_ S (Group.inverse G (Group.inverse G x)) x
diff --git a/Rings/IntegralDomains.agda b/Rings/IntegralDomains.agda
index 74b5c3f..1652b99 100644
--- a/Rings/IntegralDomains.agda
+++ b/Rings/IntegralDomains.agda
@@ -2,6 +2,7 @@
 
 open import LogicalFormulae
 open import Groups.Groups
+open import Groups.GroupDefinition
 open import Numbers.Naturals
 open import Orders
 open import Setoids.Setoids
diff --git a/Rings/RingDefinition.agda b/Rings/RingDefinition.agda
index f8f5fb7..43c2ab0 100644
--- a/Rings/RingDefinition.agda
+++ b/Rings/RingDefinition.agda
@@ -2,6 +2,7 @@
 
 open import LogicalFormulae
 open import Groups.Groups
+open import Groups.GroupDefinition
 open import Numbers.Naturals
 open import Setoids.Orders
 open import Setoids.Setoids
diff --git a/Rings/RingLemmas.agda b/Rings/RingLemmas.agda
index 35f4ba2..922e207 100644
--- a/Rings/RingLemmas.agda
+++ b/Rings/RingLemmas.agda
@@ -3,6 +3,7 @@
 open import LogicalFormulae
 open import Functions
 open import Groups.Groups
+open import Groups.GroupDefinition
 open import Groups.GroupsLemmas
 open import Rings.RingDefinition
 open import Setoids.Setoids
@@ -86,3 +87,126 @@ module Rings.RingLemmas where
       open Transitive (Equivalence.transitiveEq (Setoid.eq S))
       open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
       open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+
+  ringCanMultiplyByPositive : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → (Ring.0R R) < c → x < y → (x * c) < (y * c)
+  ringCanMultiplyByPositive {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} 0<c x<y = SetoidPartialOrder.wellDefined pOrder reflexive (Group.multIdentRight additiveGroup) q'
+    where
+      open Ring R
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      have : 0R < (y + Group.inverse additiveGroup x)
+      have = SetoidPartialOrder.wellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition oRing x<y (Group.inverse additiveGroup x))
+      p : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
+      p = SetoidPartialOrder.wellDefined pOrder reflexive (transitive multCommutative (transitive multDistributes ((Group.wellDefined additiveGroup) multCommutative multCommutative))) (OrderedRing.orderRespectsMultiplication oRing have 0<c)
+      p' : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
+      p' = SetoidPartialOrder.wellDefined pOrder reflexive (Group.wellDefined additiveGroup reflexive (transitive (transitive multCommutative (ringMinusExtracts R)) (inverseWellDefined additiveGroup multCommutative))) p
+      q : (0R + (x * c)) < (((y * c) + (Group.inverse additiveGroup (x * c))) + (x * c))
+      q = OrderedRing.orderRespectsAddition oRing p' (x * c)
+      q' : (x * c) < ((y * c) + 0R)
+      q' = SetoidPartialOrder.wellDefined pOrder (Group.multIdentLeft additiveGroup) (transitive (symmetric (Group.multAssoc additiveGroup)) (Group.wellDefined additiveGroup reflexive (Group.invLeft additiveGroup))) q
+
+  ringCanCancelPositive : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → (Ring.0R R) < c → (x * c) < (y * c) → x < y
+  ringCanCancelPositive {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} 0<c xc<yc = SetoidPartialOrder.wellDefined pOrder (Group.multIdentLeft additiveGroup) (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.multIdentRight additiveGroup))) q''
+    where
+      open Ring R
+      open Setoid S
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      have : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
+      have = SetoidPartialOrder.wellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition oRing xc<yc (Group.inverse additiveGroup _))
+      p : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
+      p = SetoidPartialOrder.wellDefined pOrder reflexive (Group.wellDefined additiveGroup reflexive (symmetric (transitive (multCommutative) (transitive (ringMinusExtracts R) (inverseWellDefined additiveGroup multCommutative))))) have
+      q : 0R < ((y + Group.inverse additiveGroup x) * c)
+      q = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (transitive (Group.wellDefined additiveGroup multCommutative multCommutative) (symmetric multDistributes)) multCommutative) p
+      q' : 0R < (y + Group.inverse additiveGroup x)
+      q' with SetoidTotalOrder.totality tOrder 0R (y + Group.inverse additiveGroup x)
+      q' | inl (inl pr) = pr
+      q' | inl (inr y-x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder reflexive (transitive multCommutative (ringTimesZero R)) k))
+        where
+          open Group additiveGroup
+          f : ((y + inverse x) + (inverse (y + inverse x))) < (identity + inverse (y + inverse x))
+          f = OrderedRing.orderRespectsAddition oRing y-x<0 _
+          g : identity < inverse (y + inverse x)
+          g = SetoidPartialOrder.wellDefined pOrder invRight multIdentLeft f
+          h : (identity * c) < ((inverse (y + inverse x)) * c)
+          h = ringCanMultiplyByPositive oRing 0<c g
+          i : (0R + (identity * c)) < (((y + inverse x) * c) + ((inverse (y + inverse x)) * c))
+          i = ringAddInequalities oRing q h
+          j : 0R < (((y + inverse x) + (inverse (y + inverse x))) * c)
+          j = SetoidPartialOrder.wellDefined pOrder (transitive multIdentLeft (transitive multCommutative (ringTimesZero R))) (symmetric (transitive multCommutative (transitive multDistributes (Group.wellDefined additiveGroup multCommutative multCommutative)))) i
+          k : 0R < (0R * c)
+          k = SetoidPartialOrder.wellDefined pOrder reflexive (multWellDefined invRight reflexive) j
+      q' | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder (multWellDefined x=y reflexive) reflexive xc<yc))
+        where
+          open Group additiveGroup
+          f : inverse identity ∼ inverse (y + inverse x)
+          f = inverseWellDefined additiveGroup 0=y-x
+          g : identity ∼ (inverse y) + x
+          g = transitive (symmetric (invIdentity additiveGroup)) (transitive f (transitive (transitive (invContravariant additiveGroup) groupIsAbelian) (wellDefined reflexive (invInv additiveGroup))))
+          x=y : x ∼ y
+          x=y = transferToRight additiveGroup (symmetric (transitive g groupIsAbelian))
+      q'' : (0R + x) < ((y + Group.inverse additiveGroup x) + x)
+      q'' = OrderedRing.orderRespectsAddition oRing q' x
+
+  ringSwapNegatives : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y : A} → (Group.inverse (Ring.additiveGroup R) x) < (Group.inverse (Ring.additiveGroup R) y) → y < x
+  ringSwapNegatives {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} oRing {x} {y} -x<-y = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.multIdentRight additiveGroup))) (Group.multIdentLeft additiveGroup) v
+    where
+      open Ring R
+      open Setoid S
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      t : ((Group.inverse additiveGroup x) + y) < ((Group.inverse additiveGroup y) + y)
+      t = OrderedRing.orderRespectsAddition oRing -x<-y y
+      u : (y + (Group.inverse additiveGroup x)) < 0R
+      u = SetoidPartialOrder.wellDefined pOrder (groupIsAbelian) (Group.invLeft additiveGroup) t
+      v : ((y + (Group.inverse additiveGroup x)) + x) < (0R + x)
+      v = OrderedRing.orderRespectsAddition oRing u x
+
+  ringCanMultiplyByNegative : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → c < (Ring.0R R) → x < y → (y * c) < (x * c)
+  ringCanMultiplyByNegative {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} c<0 x<y = ringSwapNegatives oRing u
+    where
+      open Ring R
+      open Setoid S
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      p : (c + Group.inverse additiveGroup c) < (0R + Group.inverse additiveGroup c)
+      p = OrderedRing.orderRespectsAddition oRing c<0 _
+      0<-c : 0R < (Group.inverse additiveGroup c)
+      0<-c = SetoidPartialOrder.wellDefined pOrder (Group.invRight additiveGroup) (Group.multIdentLeft additiveGroup) p
+      t : (x * Group.inverse additiveGroup c) < (y * Group.inverse additiveGroup c)
+      t = ringCanMultiplyByPositive oRing 0<-c x<y
+      u : (Group.inverse additiveGroup (x * c)) < Group.inverse additiveGroup (y * c)
+      u = SetoidPartialOrder.wellDefined pOrder (ringMinusExtracts R) (ringMinusExtracts R) t
+
+  ringCanCancelNegative : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → c < (Ring.0R R) → (x * c) < (y * c) → y < x
+  ringCanCancelNegative {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} c<0 xc<yc = r
+    where
+      open Ring R
+      open Setoid S
+      open Group additiveGroup
+      open Transitive (Equivalence.transitiveEq (Setoid.eq S))
+      open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+      open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+      p : 0R < ((y * c) + inverse (x * c))
+      p = SetoidPartialOrder.wellDefined pOrder invRight reflexive (OrderedRing.orderRespectsAddition oRing xc<yc (inverse (x * c)))
+      p1 : 0R < ((y * c) + ((inverse x) * c))
+      p1 = SetoidPartialOrder.wellDefined pOrder reflexive (Group.wellDefined additiveGroup reflexive (transitive (inverseWellDefined additiveGroup multCommutative) (transitive (symmetric (ringMinusExtracts R)) multCommutative))) p
+      p2 : 0R < ((y + inverse x) * c)
+      p2 = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (Group.wellDefined additiveGroup multCommutative multCommutative) (transitive (symmetric multDistributes) multCommutative)) p1
+      q : (y + inverse x) < 0R
+      q with SetoidTotalOrder.totality tOrder 0R (y + inverse x)
+      q | inl (inl pr) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder bad c<0))
+        where
+          bad : 0R < c
+          bad = ringCanCancelPositive oRing pr (SetoidPartialOrder.wellDefined pOrder (symmetric (transitive multCommutative (ringTimesZero R))) multCommutative p2)
+      q | inl (inr pr) = pr
+      q | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder (multWellDefined x=y reflexive) reflexive xc<yc))
+        where
+          x=y : x ∼ y
+          x=y = transitive (symmetric multIdentLeft) (transitive (Group.wellDefined additiveGroup 0=y-x reflexive) (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive invLeft) multIdentRight)))
+      r : y < x
+      r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive (invLeft)) multIdentRight)) (Group.multIdentLeft additiveGroup) (OrderedRing.orderRespectsAddition oRing q x)