diff --git a/Fields/CauchyCompletion/Addition.agda b/Fields/CauchyCompletion/Addition.agda
index 6e12dd1..7313a3e 100644
--- a/Fields/CauchyCompletion/Addition.agda
+++ b/Fields/CauchyCompletion/Addition.agda
@@ -47,7 +47,7 @@ CauchyCompletion.converges (record { elts = a ; converges = convA } +C record {
     t {m} {n} <m <n with prA {m} {n} (inequalityShrinkLeft <m) (inequalityShrinkLeft <n)
     ... | am-an<e/2 with prB {m} {n} (inequalityShrinkRight <m) (inequalityShrinkRight <n)
     ... | bm-bn<e/2 with triangleInequality (index a m + inverse (index a n)) (index b m + inverse (index b n))
-    ... | inl tri rewrite lemm m a b | lemm n a b = SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive eq) e/2Pr (SetoidPartialOrder.transitive pOrder {_} {(abs ((index a m) + (inverse (index a n)))) + (abs ((index b m) + (inverse (index b n))))} (<WellDefined (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index a m})) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq {index a m}) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index b m})) (+WellDefined (Equivalence.reflexive eq {index b m}) (Equivalence.symmetric eq (invContravariant additiveGroup)))))) (+Associative {index a m})))) (Equivalence.reflexive eq) tri) (ringAddInequalities am-an<e/2 bm-bn<e/2))
+    ... | inl tri rewrite lemm m a b | lemm n a b = SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive eq) e/2Pr (SetoidPartialOrder.<Transitive pOrder {_} {(abs ((index a m) + (inverse (index a n)))) + (abs ((index b m) + (inverse (index b n))))} (<WellDefined (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index a m})) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq {index a m}) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index b m})) (+WellDefined (Equivalence.reflexive eq {index b m}) (Equivalence.symmetric eq (invContravariant additiveGroup)))))) (+Associative {index a m})))) (Equivalence.reflexive eq) tri) (ringAddInequalities am-an<e/2 bm-bn<e/2))
     ... | inr tri rewrite lemm m a b | lemm n a b = SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive eq) e/2Pr (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq tri) (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index a m})) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq {index a m}) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index b m})) (+WellDefined (Equivalence.reflexive eq {index b m}) (Equivalence.symmetric eq (invContravariant additiveGroup)))))) (+Associative {index a m}))))) (Equivalence.reflexive eq) (ringAddInequalities am-an<e/2 bm-bn<e/2))
 
 inverseDistributes : {r s : A} → inverse (r + s) ∼ inverse r + inverse s
diff --git a/Fields/CauchyCompletion/Approximation.agda b/Fields/CauchyCompletion/Approximation.agda
index f8fcf03..408ba72 100644
--- a/Fields/CauchyCompletion/Approximation.agda
+++ b/Fields/CauchyCompletion/Approximation.agda
@@ -42,7 +42,7 @@ open import Fields.CauchyCompletion.Comparison order F charNot2
 abstract
 
   chain : {a b : A} (c : CauchyCompletion) → (a r<C c) → (c <Cr b) → a < b
-  chain {a} {b} c (betweenAC , (0<betweenAC ,, (Nac , prAC))) (betweenCB , (0<betweenCB ,, (Nb , prBC))) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenAC a)) (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (prAC (succ Nac +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Nac)))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenCB (index (Sequence.tail (CauchyCompletion.elts c)) (Nac +N Nb))))))) (prBC (succ Nac +N Nb) (le Nac refl))
+  chain {a} {b} c (betweenAC , (0<betweenAC ,, (Nac , prAC))) (betweenCB , (0<betweenCB ,, (Nb , prBC))) = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenAC a)) (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (prAC (succ Nac +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Nac)))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenCB (index (Sequence.tail (CauchyCompletion.elts c)) (Nac +N Nb))))))) (prBC (succ Nac +N Nb) (le Nac refl))
 
   approxLemma : (a : CauchyCompletion) (e e/2 : A) → (0G < e) → (e/2 + e/2 ∼ e) → (m N : ℕ) → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N)) < e/2 → (e/2 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) N + e)
   approxLemma a e e/2 0<e prE/2 m N ans with totality 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N))
@@ -63,7 +63,7 @@ abstract
       ans m N<m | bl | inl (inl 0<am-aN) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (Equivalence.reflexive eq) (orderRespectsAddition bl (index (CauchyCompletion.elts a) (succ N)))
       ... | am<1+an = <WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) identLeft) groupIsAbelian) (Equivalence.transitive eq (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) +Associative) (ringAddInequalities am<1+an (orderRespectsAddition (0<1 (charNot2ImpliesNontrivial R charNot2)) 1R))
       ans m N<m | bl | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
-      ... | am<aN = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.transitive pOrder am<aN (<WellDefined (Equivalence.reflexive eq) (+Associative) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (0<1 (charNot2ImpliesNontrivial R charNot2)) (0<1 (charNot2ImpliesNontrivial R charNot2)))) (index (CauchyCompletion.elts a) (succ N)))))) 1R)
+      ... | am<aN = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder am<aN (<WellDefined (Equivalence.reflexive eq) (+Associative) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (0<1 (charNot2ImpliesNontrivial R charNot2)) (0<1 (charNot2ImpliesNontrivial R charNot2)))) (index (CauchyCompletion.elts a) (succ N)))))) 1R)
       ans m N<m | bl | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (+WellDefined identLeft (Equivalence.reflexive eq)) identLeft) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (Equivalence.reflexive eq)) +Associative)) (orderRespectsAddition (ringAddInequalities (0<1 (charNot2ImpliesNontrivial R charNot2)) (0<1 (charNot2ImpliesNontrivial R charNot2))) (1R + (index (CauchyCompletion.elts a) m)))
 
   rationalApproximatelyAbove : (a : CauchyCompletion) → (e : A) → (0G < e) → A
@@ -88,13 +88,13 @@ abstract
       ans2 : (m : ℕ) → N +N N2 <N m → (e/8 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N) + e/2)
       ans2 m <m with cauchyBeyondN {m} {succ N} (inequalityShrinkLeft <m) (le 0 refl)
       ... | absam-aN<e/4 with totality 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) (succ N)))
-      ans2 m <m | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian (Equivalence.transitive eq groupIsAbelian  +Associative) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) (Equivalence.reflexive eq) (orderRespectsAddition am-aN<e/4 (index (CauchyCompletion.elts a) (succ N)))) e/8)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)) (index (CauchyCompletion.elts a) (succ N))))
+      ans2 m <m | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian (Equivalence.transitive eq groupIsAbelian  +Associative) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) (Equivalence.reflexive eq) (orderRespectsAddition am-aN<e/4 (index (CauchyCompletion.elts a) (succ N)))) e/8)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)) (index (CauchyCompletion.elts a) (succ N))))
       ans2 m <m | -[am-aN]<e/4 | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft)) (Equivalence.reflexive eq) (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _) (ringSwapNegatives' -[am-aN]<e/4)) (e/4 + e/8))
-      ... | e/8<am-aN+e/4+e/8 = SetoidPartialOrder.transitive pOrder (orderRespectsAddition e/8<am-aN+e/4+e/8 (index (CauchyCompletion.elts a) m)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities am-aN<0 (<WellDefined groupIsAbelian prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)))) am<aN))
+      ... | e/8<am-aN+e/4+e/8 = SetoidPartialOrder.<Transitive pOrder (orderRespectsAddition e/8<am-aN+e/4+e/8 (index (CauchyCompletion.elts a) m)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities am-aN<0 (<WellDefined groupIsAbelian prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)))) am<aN))
         where
           am<aN : (index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N))
           am<aN = <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) groupIsAbelian)) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invRight) identRight)) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
-      ans2 m <m | absam-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (orderRespectsAddition {b = e/2} (SetoidPartialOrder.transitive pOrder (halfLess e/8 e/4 0<e/4 prE/8) (halfLess e/4 e/2 0<e/2 prE/4)) (index (CauchyCompletion.elts a) m))
+      ans2 m <m | absam-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (orderRespectsAddition {b = e/2} (SetoidPartialOrder.<Transitive pOrder (halfLess e/8 e/4 0<e/4 prE/8) (halfLess e/4 e/2 0<e/2 prE/4)) (index (CauchyCompletion.elts a) m))
 
   rationalApproximatelyAboveIsNear : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → (injection (rationalApproximatelyAbove a e 0<e) +C (-C a)) <C (injection e)
   rationalApproximatelyAboveIsNear a e 0<e with halve charNot2 e
@@ -121,7 +121,7 @@ abstract
           r : ((inverse am) + aN) < e/4
           r with t
           ... | f with totality 0G (am + inverse aN)
-          r | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) (lemm2' _ 0<am-aN)) 0<e/4
+          r | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) (lemm2' _ 0<am-aN)) 0<e/4
           r | f | inl (inr x) = <WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) f
           r | am-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq 0=am-aN) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invIdentity additiveGroup)) (inverseWellDefined additiveGroup 0=am-aN)) (inverseWellDefined additiveGroup groupIsAbelian)) (invContravariant additiveGroup)) (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) am-aN<e/4
           q : ((inverse (index (CauchyCompletion.elts a) m)) + (index (CauchyCompletion.elts a) (succ N) + e/2)) < (e/4 + e/2)
@@ -145,56 +145,56 @@ abstract
   ... | below , (below<a ,, a-below<e) with approximateAbove a 1R (0<1 (charNot2ImpliesNontrivial R charNot2))
   ... | above , (a<above ,, above-a<e) with totality 0R below
   boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) with totality 0R above
-  boundModulus a | below , ((belowBound , (0<belowBound ,, (Nbelow , prBelow))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inl (inl 0<below) | inl (inl 0<above) = above , ((N +N Nbelow) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
+  boundModulus a | below , ((belowBound , (0<belowBound ,, (Nbelow , prBelow))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inl (inl 0<below) | inl (inl 0<above) = above , ((N +N Nbelow) , λ m N<m → SetoidPartialOrder.<Transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
     where
       res : (m : ℕ) → ((N +N Nbelow) <N m) → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
       res m N<m with totality 0R (index (CauchyCompletion.elts a) m)
       res m N<m | inl (inl _) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
-      res m N<m | inl (inr am<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<belowBound below)) (prBelow m (inequalityShrinkRight N<m))) am<0)))
+      res m N<m | inl (inr am<0) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 0<below (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<belowBound below)) (prBelow m (inequalityShrinkRight N<m))) am<0)))
       res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
-  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inl (inr above<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (chain a below<a a<above) above<0)))
-  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inr 0=above = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (chain a below<a a<above))))
+  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inl (inr above<0) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 0<below (SetoidPartialOrder.<Transitive pOrder (chain a below<a a<above) above<0)))
+  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inr 0=above = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 0<below (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (chain a below<a a<above))))
   boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) with totality 0R above
   boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) with totality (inverse below) above
   boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inl -bel<ab) = above , ((N +N Nabove) , ans)
     where
       ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
       ans m N<m with totality 0G (index (CauchyCompletion.elts a) m)
-      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
-      ans m N<m | inl (inr am<0) = SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (prBoundBelow m (inequalityShrinkLeft N<m))) (SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below))) -bel<ab)
+      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
+      ans m N<m | inl (inr am<0) = SetoidPartialOrder.<Transitive pOrder (ringSwapNegatives' (prBoundBelow m (inequalityShrinkLeft N<m))) (SetoidPartialOrder.<Transitive pOrder (ringSwapNegatives' (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below))) -bel<ab)
       ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
   boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inr ab<-bel) = inverse below , ((N +N Nabove) , ans)
     where
       ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < (inverse below)
       ans m N<m with totality 0G (index (CauchyCompletion.elts a) m)
-      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) ab<-bel
-      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
+      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) ab<-bel
+      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
       ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 below below<0)
   boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inr -bel=ab = above , ((N +N Nabove) , ans)
     where
       ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
       ans m N<m with totality 0G (index (CauchyCompletion.elts a) m)
-      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
-      ans m N<m | inl (inr am<0) = <WellDefined (Equivalence.reflexive eq) (-bel=ab) (ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m))))
+      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
+      ans m N<m | inl (inr am<0) = <WellDefined (Equivalence.reflexive eq) (-bel=ab) (ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m))))
       ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
   boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inr above<0) = inverse below , ((N +N Nabove) , ans)
     where
       ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
       ans m N<m with totality 0R (index (CauchyCompletion.elts a) m)
-      ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
-      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
-      ans m N<m | inr 0=am = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=am) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
+      ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<am (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
+      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
+      ans m N<m | inr 0=am = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=am) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
   boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inr 0=above = inverse below , ((N +N Nabove) , ans)
     where
       ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
       ans m N<m with totality 0R (index (CauchyCompletion.elts a) m)
-      ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))))))
-      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
+      ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (SetoidPartialOrder.<Transitive pOrder 0<am (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))))))
+      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
       ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 _ below<0)
-  boundModulus a | below , ((boundBelow , ((boundBelowDiff ,, (Nb , ansBelow)))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inr 0=below = above , ((N +N Nb) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
+  boundModulus a | below , ((boundBelow , ((boundBelowDiff ,, (Nb , ansBelow)))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inr 0=below = above , ((N +N Nb) , λ m N<m → SetoidPartialOrder.<Transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
     where
       res : (m : ℕ) → (N +N Nb) <N m → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
       res m N<m with totality 0R (index (CauchyCompletion.elts a) m)
       res m N<m | inl (inl 0<am) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
-      res m N<m | inl (inr am<0) = exFalso (irreflexive (<WellDefined (Equivalence.symmetric eq 0=below) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition boundBelowDiff below)) (ansBelow m (inequalityShrinkRight N<m))) am<0)))
+      res m N<m | inl (inr am<0) = exFalso (irreflexive (<WellDefined (Equivalence.symmetric eq 0=below) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition boundBelowDiff below)) (ansBelow m (inequalityShrinkRight N<m))) am<0)))
       res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
diff --git a/Fields/CauchyCompletion/Comparison.agda b/Fields/CauchyCompletion/Comparison.agda
index f03fef5..ef6b686 100644
--- a/Fields/CauchyCompletion/Comparison.agda
+++ b/Fields/CauchyCompletion/Comparison.agda
@@ -63,7 +63,7 @@ a <Cr b = Sg A (λ ε → (0G < ε) && Sg ℕ (λ N → ((m : ℕ) → (N<m : N
   where
     ans : (m : ℕ) → (N<m : (N +N N2) <N m) → (e/2 + index (CauchyCompletion.elts b) m) < c
     ans m N<m with prN2 {m} (shrinkInequality' N<m)
-    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = SetoidPartialOrder.transitive pOrder (<CrWellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) e/2 ε 0<e prE/2 bl) (pr m (shrinkInequality N<m))
+    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = SetoidPartialOrder.<Transitive pOrder (<CrWellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) e/2 ε 0<e prE/2 bl) (pr m (shrinkInequality N<m))
 
 <CrWellDefined : (a b : CauchyCompletion) (c d : A) → Setoid._∼_ cauchyCompletionSetoid a b → c ∼ d → a <Cr c → b <Cr d
 <CrWellDefined a b c d a=b c=d a<c = <CrWellDefinedLeft a b d a=b (<CrWellDefinedRight a c d c=d a<c)
@@ -76,9 +76,9 @@ r<CWellDefinedLeft a b c a=b (e , (0<e ,, (N , pr))) = e , (0<e ,, (N , λ m N<m
 
 r<CWellDefinedLemma : (a b c e e/2 : A) (_ : e/2 + e/2 ∼ e) (0<e : 0G < e) (_ : abs (a + inverse b) < e/2) (_ : (c + e) < a) → (c + e/2) < b
 r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a with totality 0G (a + inverse b)
-r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inl 0<a-b) = SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq prE/2) (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invRight)) identRight)))) (Equivalence.reflexive eq) (orderRespectsAddition c+e<a (inverse e/2))) (<WellDefined (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (Equivalence.reflexive eq))) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (invLeft)) identRight))) (orderRespectsAddition pr (b + inverse e/2)))
-r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inr a-b<0) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) c+e<a) (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition a-b<0 b))
-r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inr 0=a-b = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) (<WellDefined (groupIsAbelian {c} {e}) (transferToRight additiveGroup (Equivalence.symmetric eq 0=a-b)) c+e<a)
+r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inl 0<a-b) = SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq prE/2) (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invRight)) identRight)))) (Equivalence.reflexive eq) (orderRespectsAddition c+e<a (inverse e/2))) (<WellDefined (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (Equivalence.reflexive eq))) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (invLeft)) identRight))) (orderRespectsAddition pr (b + inverse e/2)))
+r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inr a-b<0) = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) c+e<a) (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition a-b<0 b))
+r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inr 0=a-b = SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) (<WellDefined (groupIsAbelian {c} {e}) (transferToRight additiveGroup (Equivalence.symmetric eq 0=a-b)) c+e<a)
 
 r<CWellDefinedRight : (a b : CauchyCompletion) (c : A) → Setoid._∼_ cauchyCompletionSetoid a b → c r<C a → c r<C b
 r<CWellDefinedRight a b c a=b (e , (0<e ,, (N , pr))) with halve charNot2 e
@@ -114,18 +114,18 @@ r<CPreserves {a} {b} a<b with dense charNot2 a<b
 <CInherited' : {a b : A} → (injection a) <C (injection b) → a < b
 <CInherited' {a} {b} (bound , ((Na , (0<Na ,, (Na2 , prA))) ,, ((Nb , (0<Nb ,, (Nb2 , prB)))))) with prA (succ Na2) (le 0 refl)
 ... | bl with prB (succ Nb2) (le 0 refl)
-... | bl2 rewrite indexAndConst a Na2 | indexAndConst b Nb2 = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<Na a)) bl) (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<Nb bound)) bl2)
+... | bl2 rewrite indexAndConst a Na2 | indexAndConst b Nb2 = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<Na a)) bl) (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<Nb bound)) bl2)
 
 <CIrreflexive : {a : CauchyCompletion} → a <C a → False
 <CIrreflexive {a} (bound , ((bA , (0<bA ,, (Na , prA))) ,, ((bB , (0<bB ,, (Nb , prB)))))) with prA (succ Na +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Na)))
 ... | bl with prB (succ Na +N Nb) (le Na refl)
 ... | bl2 with <WellDefined (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) groupIsAbelian) (Equivalence.reflexive eq))) groupIsAbelian (ringAddInequalities bl bl2)
-... | bad = irreflexive (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft +Associative (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<bA 0<bB)) (index (CauchyCompletion.elts a) (succ Na +N Nb) + bound)))) bad)
+... | bad = irreflexive (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft +Associative (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<bA 0<bB)) (index (CauchyCompletion.elts a) (succ Na +N Nb) + bound)))) bad)
 
 <CTransitive : {a b c : CauchyCompletion} → a <C b → b <C c → a <C c
-<CTransitive {a} {b} {c} (boundA , ((eL , (0<eL ,, prL)) ,, (eR , (0<eR ,, (Nr , prR))))) (boundB , ((fL , (0<fL ,, (Nfl , prFl))) ,, (fR , (0<fR ,, (N , prFR))))) = boundA , ((eL , (0<eL ,, prL)) ,, (eR , (0<eR ,, (((Nr +N Nfl) +N N) , λ m N<m → SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (prR m (shrinkInequality {Nr} (shrinkInequality N<m))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<fL (index (CauchyCompletion.elts b) m)))) (prFl m (shrinkInequality' {Nr} (shrinkInequality N<m)))) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<fR boundB))) (prFR m (shrinkInequality' N<m))))))
+<CTransitive {a} {b} {c} (boundA , ((eL , (0<eL ,, prL)) ,, (eR , (0<eR ,, (Nr , prR))))) (boundB , ((fL , (0<fL ,, (Nfl , prFl))) ,, (fR , (0<fR ,, (N , prFR))))) = boundA , ((eL , (0<eL ,, prL)) ,, (eR , (0<eR ,, (((Nr +N Nfl) +N N) , λ m N<m → SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (prR m (shrinkInequality {Nr} (shrinkInequality N<m))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<fL (index (CauchyCompletion.elts b) m)))) (prFl m (shrinkInequality' {Nr} (shrinkInequality N<m)))) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<fR boundB))) (prFR m (shrinkInequality' N<m))))))
 
 <COrder : SetoidPartialOrder cauchyCompletionSetoid _<C_
 SetoidPartialOrder.<WellDefined <COrder {a} {b} {c} {d} a=b c=d a<c = <CWellDefined {a} {b} {c} {d} a=b c=d a<c
 SetoidPartialOrder.irreflexive <COrder {a} a<a = <CIrreflexive {a} a<a
-SetoidPartialOrder.transitive <COrder {a} {b} {c} a<b b<c = <CTransitive {a} {b} {c} a<b b<c
+SetoidPartialOrder.<Transitive <COrder {a} {b} {c} a<b b<c = <CTransitive {a} {b} {c} a<b b<c
diff --git a/Fields/CauchyCompletion/Multiplication.agda b/Fields/CauchyCompletion/Multiplication.agda
index 9bf7fb5..db8389a 100644
--- a/Fields/CauchyCompletion/Multiplication.agda
+++ b/Fields/CauchyCompletion/Multiplication.agda
@@ -115,17 +115,17 @@ CauchyCompletion.converges (record { elts = a ; converges = aConv } *C record {
         p : ((abs (index a m) * abs (index b m + inverse (index b n))) + (abs (index b n) * abs (index a m + inverse (index a n)))) < e
         p with totality 0R (index b m + inverse (index b n))
         p | inl (inl 0<bm-bn) with totality 0R (index a m + inverse (index a n))
-        p | inl (inl 0<bm-bn) | inl (inl 0<am-an) = SetoidPartialOrder.transitive pOrder (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn)) (ringCanMultiplyByPositive 0<bm-bn (SetoidPartialOrder.transitive pOrder (prABound m Na<m) ab<bb))) (<WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<am-an)) (ringCanMultiplyByPositive 0<am-an (SetoidPartialOrder.transitive pOrder (prBBound n Nb<n) bb<bb)))) q
-        p | inl (inl 0<bm-bn) | inl (inr am-an<0) = SetoidPartialOrder.transitive pOrder (ringAddInequalities (<WellDefined (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (greaterZeroImpliesEqualAbs 0<bm-bn))) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn) 0<bm-bn) (SetoidPartialOrder.transitive pOrder (prABound m Na<m) ab<bb))) (<WellDefined (*WellDefined (Equivalence.reflexive eq) (lessZeroImpliesEqualNegAbs am-an<0)) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lessZeroImpliesEqualNegAbs am-an<0)) (lemm2 _ am-an<0)) (SetoidPartialOrder.transitive pOrder (prBBound n Nb<n) bb<bb)))) q
-        p | inl (inl 0<bm-bn) | inr 0=am-an = <WellDefined (+WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) 0=am-an)) (Equivalence.reflexive eq) (<WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq timesZero)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq identRight) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq absZeroIsZero) (absWellDefined _ _ 0=am-an)))) (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq timesZero)) (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq identRight) (<WellDefined (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (greaterZeroImpliesEqualAbs 0<bm-bn))) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn) 0<bm-bn) (SetoidPartialOrder.transitive pOrder (prABound m Na<m) ab<bb)))))) q)))
-        p | inl (inr bm-bn<0) = SetoidPartialOrder.transitive pOrder ans'' q
+        p | inl (inl 0<bm-bn) | inl (inl 0<am-an) = SetoidPartialOrder.<Transitive pOrder (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn)) (ringCanMultiplyByPositive 0<bm-bn (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) ab<bb))) (<WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<am-an)) (ringCanMultiplyByPositive 0<am-an (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb)))) q
+        p | inl (inl 0<bm-bn) | inl (inr am-an<0) = SetoidPartialOrder.<Transitive pOrder (ringAddInequalities (<WellDefined (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (greaterZeroImpliesEqualAbs 0<bm-bn))) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn) 0<bm-bn) (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) ab<bb))) (<WellDefined (*WellDefined (Equivalence.reflexive eq) (lessZeroImpliesEqualNegAbs am-an<0)) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lessZeroImpliesEqualNegAbs am-an<0)) (lemm2 _ am-an<0)) (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb)))) q
+        p | inl (inl 0<bm-bn) | inr 0=am-an = <WellDefined (+WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) 0=am-an)) (Equivalence.reflexive eq) (<WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq timesZero)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq identRight) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq absZeroIsZero) (absWellDefined _ _ 0=am-an)))) (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq timesZero)) (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq identRight) (<WellDefined (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (greaterZeroImpliesEqualAbs 0<bm-bn))) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn) 0<bm-bn) (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) ab<bb)))))) q)))
+        p | inl (inr bm-bn<0) = SetoidPartialOrder.<Transitive pOrder ans'' q
           where
             bar : ((abs (index a m)) * (inverse (index b m + inverse (index b n)))) < (boundBoth * abs (index b m + inverse (index b n)))
-            bar = <WellDefined (*WellDefined (Equivalence.reflexive eq) (lessZeroImpliesEqualNegAbs bm-bn<0)) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lessZeroImpliesEqualNegAbs bm-bn<0)) (lemm2 _ bm-bn<0)) (SetoidPartialOrder.transitive pOrder (prABound m Na<m) (ab<bb)))
+            bar = <WellDefined (*WellDefined (Equivalence.reflexive eq) (lessZeroImpliesEqualNegAbs bm-bn<0)) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lessZeroImpliesEqualNegAbs bm-bn<0)) (lemm2 _ bm-bn<0)) (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) (ab<bb)))
             foo : (((abs (index b n)) * (abs (index a m + inverse (index a n)))) < (boundBoth * abs (index a m + inverse (index a n)))) || (((abs (index b n)) * (abs (index a m + inverse (index a n)))) ∼ (boundBoth * abs (index a m + inverse (index a n))))
             foo with totality 0R (index a m + inverse (index a n))
-            foo | inl (inl 0<am-an) = inl (ringCanMultiplyByPositive 0<am-an (SetoidPartialOrder.transitive pOrder (prBBound n Nb<n) bb<bb))
-            foo | inl (inr am-an<0) = inl (ringCanMultiplyByPositive (lemm2 _ am-an<0) (SetoidPartialOrder.transitive pOrder (prBBound n Nb<n) bb<bb))
+            foo | inl (inl 0<am-an) = inl (ringCanMultiplyByPositive 0<am-an (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb))
+            foo | inl (inr am-an<0) = inl (ringCanMultiplyByPositive (lemm2 _ am-an<0) (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb))
             foo | inr 0=am-an = inr (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=am-an)) (Equivalence.transitive eq (Equivalence.transitive eq timesZero (Equivalence.symmetric eq timesZero)) (*WellDefined (Equivalence.reflexive eq) 0=am-an)))
             ans'' : _
             ans'' with foo
@@ -139,16 +139,16 @@ CauchyCompletion.converges (record { elts = a ; converges = aConv } *C record {
             bar' = Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=bm-bn)) timesZero
             foo : (((abs (index b n)) * (abs (index a m + inverse (index a n)))) < (boundBoth * abs (index a m + inverse (index a n)))) || (0R ∼ (index a m + inverse (index a n)))
             foo with totality 0R (index a m + inverse (index a n))
-            foo | inl (inl 0<am-an) = inl (SetoidPartialOrder.transitive pOrder (ringCanMultiplyByPositive 0<am-an (prBBound n Nb<n)) (ringCanMultiplyByPositive 0<am-an bb<bb))
-            foo | inl (inr am-an<0) = inl (SetoidPartialOrder.transitive pOrder (ringCanMultiplyByPositive (lemm2 _ am-an<0) (prBBound n Nb<n)) (ringCanMultiplyByPositive (lemm2 _ am-an<0) bb<bb))
+            foo | inl (inl 0<am-an) = inl (SetoidPartialOrder.<Transitive pOrder (ringCanMultiplyByPositive 0<am-an (prBBound n Nb<n)) (ringCanMultiplyByPositive 0<am-an bb<bb))
+            foo | inl (inr am-an<0) = inl (SetoidPartialOrder.<Transitive pOrder (ringCanMultiplyByPositive (lemm2 _ am-an<0) (prBBound n Nb<n)) (ringCanMultiplyByPositive (lemm2 _ am-an<0) bb<bb))
             foo | inr 0=am-an = inr 0=am-an
             ans'' : _
             ans'' with foo
-            ... | inl pr = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (<WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bar')) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bar)) (orderRespectsAddition pr 0R))) q
+            ... | inl pr = SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (<WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bar')) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bar)) (orderRespectsAddition pr 0R))) q
             ... | inr pr = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.symmetric eq bar') (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.symmetric eq pr)) absZeroIsZero)) timesZero)))) (Equivalence.reflexive eq) 0<e
         ans' : abs ((index a m * index b m) + inverse (index a n * index b n)) < e
         ans' with triangleInequality (index a m * (index b m + inverse (index b n))) (index b n * (index a m + inverse (index a n)))
-        ... | inl less = <WellDefined (Equivalence.symmetric eq (absWellDefined ((index a m * index b m) + (inverse (index a n * index b n))) (((index a m) * (index b m + (inverse (index b n)))) + ((index b n) * (index a m + inverse (index a n)))) littleLemma)) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder less (<WellDefined (+WellDefined (Equivalence.symmetric eq (absRespectsTimes (index a m) _)) (Equivalence.symmetric eq (absRespectsTimes (index b n) _))) (Equivalence.reflexive eq) p))
+        ... | inl less = <WellDefined (Equivalence.symmetric eq (absWellDefined ((index a m * index b m) + (inverse (index a n * index b n))) (((index a m) * (index b m + (inverse (index b n)))) + ((index b n) * (index a m + inverse (index a n)))) littleLemma)) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder less (<WellDefined (+WellDefined (Equivalence.symmetric eq (absRespectsTimes (index a m) _)) (Equivalence.symmetric eq (absRespectsTimes (index b n) _))) (Equivalence.reflexive eq) p))
         ... | inr equal rewrite indexAndApply a b _*_ {m} | indexAndApply a b _*_ {n} = <WellDefined (Equivalence.symmetric eq (absWellDefined ((index a m * index b m) + (inverse (index a n * index b n))) (((index a m) * (index b m + (inverse (index b n)))) + ((index b n) * (index a m + inverse (index a n)))) littleLemma)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq equal) (Equivalence.reflexive eq) ((<WellDefined (+WellDefined (Equivalence.symmetric eq (absRespectsTimes (index a m) _)) (Equivalence.symmetric eq (absRespectsTimes (index b n) _))) (Equivalence.reflexive eq) p)))
 
 *CCommutative : {a b : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a *C b) (b *C a)
@@ -178,7 +178,7 @@ abstract
       0<cBound : 0G < cBound
       0<cBound with totality 0G cBound
       0<cBound | inl (inl 0<cBound) = 0<cBound
-      0<cBound | inl (inr cBound<0) = exFalso (absNonnegative (SetoidPartialOrder.transitive pOrder (cBoundPr (succ cBoundN) (le 0 refl)) cBound<0))
+      0<cBound | inl (inr cBound<0) = exFalso (absNonnegative (SetoidPartialOrder.<Transitive pOrder (cBoundPr (succ cBoundN) (le 0 refl)) cBound<0))
       0<cBound | inr 0=cBound = exFalso (absNonnegative (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=cBound) (cBoundPr (succ cBoundN) (le 0 refl))))
       e/c : A
       e/c with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
diff --git a/Fields/CauchyCompletion/Setoid.agda b/Fields/CauchyCompletion/Setoid.agda
index 5884f40..ee0a1ed 100644
--- a/Fields/CauchyCompletion/Setoid.agda
+++ b/Fields/CauchyCompletion/Setoid.agda
@@ -39,7 +39,7 @@ isZero record { elts = elts ; converges = converges } = ∀ ε → 0R < ε → S
 
 transitiveLemma : {a b c e/2 : A} → abs (a + inverse b) < e/2 → abs (b + inverse c) < e/2 → (abs (a + inverse c)) < (e/2 + e/2)
 transitiveLemma {a} {b} {c} {e/2} a-b<e/2 b-c<e/2 with triangleInequality (a + inverse b) (b + inverse c)
-transitiveLemma {a} {b} {c} {e/2} a-b<e/2 b-c<e/2 | inl x = SetoidPartialOrder.transitive pOrder (<WellDefined (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft))))) (Equivalence.reflexive eq) x) (ringAddInequalities a-b<e/2 b-c<e/2)
+transitiveLemma {a} {b} {c} {e/2} a-b<e/2 b-c<e/2 | inl x = SetoidPartialOrder.<Transitive pOrder (<WellDefined (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft))))) (Equivalence.reflexive eq) x) (ringAddInequalities a-b<e/2 b-c<e/2)
 transitiveLemma {a} {b} {c} {e/2} a-b<e/2 b-c<e/2 | inr x = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.symmetric eq ((Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft))))))) x)) (Equivalence.reflexive eq) (ringAddInequalities a-b<e/2 b-c<e/2)
 
 cauchyCompletionSetoid : Setoid CauchyCompletion
diff --git a/Fields/FieldOfFractionsOrder.agda b/Fields/FieldOfFractionsOrder.agda
index 21e5f2d..5db7fb4 100644
--- a/Fields/FieldOfFractionsOrder.agda
+++ b/Fields/FieldOfFractionsOrder.agda
@@ -62,7 +62,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       r = SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) *Commutative) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) q
       s : (numZ * denomY) < (numY * denomZ)
       s = ringCanCancelPositive order 0<denomX r
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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 Equivalence (Setoid.eq S)
@@ -77,12 +77,12 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       q = SetoidPartialOrder.<WellDefined pOrder reflexive (*WellDefined x=z reflexive) p
       r : ((numY * denomZ) * denomX) < ((numZ * denomY) * denomX)
       r = SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive (symmetric *Associative) *Commutative) q
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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 (Equivalence.symmetric (Setoid.eq S) x))
   fieldOfFractionsOrderWellDefinedLeft {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 (Equivalence.symmetric (Setoid.eq S) 0=denomX))
   fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomX
   fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomY
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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
@@ -95,7 +95,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       r = SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive (symmetric *Associative) *Commutative) q
   fieldOfFractionsOrderWellDefinedLeft {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 (Equivalence.symmetric (Setoid.eq S) x))
   fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomY
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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
@@ -116,7 +116,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       open Equivalence (Setoid.eq S)
       p : ((numY * denomX) * denomZ) < ((denomY * numX) * denomZ)
       p = ringCanMultiplyByNegative pRing denomZ<0 (SetoidPartialOrder.<WellDefined pOrder *Commutative reflexive x<y)
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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 (Equivalence.symmetric (Setoid.eq S) x))
   fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomY
   fieldOfFractionsOrderWellDefinedLeft {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 *Associative) (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined x=z reflexive) (transitive (symmetric *Associative) *Commutative))))) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) p)
@@ -125,21 +125,21 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       open Equivalence (Setoid.eq S)
       p : ((numX * denomY) * denomZ) < ((numY * denomX) * denomZ)
       p = ringCanMultiplyByNegative pRing denomZ<0 x<y
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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 (Equivalence.symmetric (Setoid.eq S) 0=denomY))
   fieldOfFractionsOrderWellDefinedLeft {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 Equivalence (Setoid.eq S)
   fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomX
   fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomY
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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 (*WellDefined *Commutative reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive x=z) (transitive *Associative (transitive *Commutative *Associative))))) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (ringCanMultiplyByNegative pRing denomZ<0 x<y))
     where
       open Ring R
       open Equivalence (Setoid.eq S)
   fieldOfFractionsOrderWellDefinedLeft {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 (Equivalence.symmetric (Setoid.eq S) x))
   fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomY
-  fieldOfFractionsOrderWellDefinedLeft {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 {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 {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 *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive (*WellDefined *Commutative reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive x=z) (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (*WellDefined *Commutative reflexive)))))) (ringCanMultiplyByNegative pRing denomZ<0 x<y))
     where
       open Ring R
@@ -213,18 +213,18 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr with totality (Ring.0R R) aDenom
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) with totality (Ring.0R R) aDenom
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inl (inl _) = SetoidPartialOrder.irreflexive pOrder pr
-  SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {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) {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) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inr x = exFalso (aDenom!=0 (Equivalence.symmetric (Setoid.eq S) x))
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) with totality (Ring.0R R) aDenom
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inl (inl 0<aDenom) = SetoidPartialOrder.irreflexive pOrder pr
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inl (inr _) = SetoidPartialOrder.irreflexive pOrder pr
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inr x = exFalso (aDenom!=0 (Equivalence.symmetric (Setoid.eq S) x))
   SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inr x = exFalso (aDenom!=0 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c with totality (Ring.0R R) denomA
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) with totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 order 0<denomB p
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c with totality (Ring.0R R) denomA
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) with totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 order 0<denomB p
     where
       open Setoid S
       open Ring R
@@ -232,32 +232,32 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       inter : ((numA * denomB) * denomC) < ((numB * denomA) * denomC)
       inter = ringCanMultiplyByPositive pRing 0<denomC a<b
       p : ((numA * denomC) * denomB) < ((numC * denomA) * denomB)
-      p = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) reflexive inter) (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (ringCanMultiplyByPositive pRing 0<denomA b<c))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 order denomB<0 (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) reflexive (ringCanMultiplyByPositive pRing 0<denomA b<c)) (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (ringCanMultiplyByPositive pRing 0<denomC a<b)))
+      p = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) reflexive inter) (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (ringCanMultiplyByPositive pRing 0<denomA b<c))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 order denomB<0 (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) reflexive (ringCanMultiplyByPositive pRing 0<denomA b<c)) (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (ringCanMultiplyByPositive pRing 0<denomC a<b)))
     where
       open Setoid S
       open Ring R
       open Equivalence (Setoid.eq S)
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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) {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 order 0<denomB (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomC<0 a<b)))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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) {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 order 0<denomB (SetoidPartialOrder.<Transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomC<0 a<b)))
     where
       open Setoid S
       open Ring R
       open Equivalence (Setoid.eq S)
       have : ((numC * denomA) * denomB) < ((numB * denomC)  * denomA)
       have = SetoidPartialOrder.<WellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByPositive pRing 0<denomA b<c)
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  ... | (inl (inl 0<denomC)) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
-  ... | (inl (inr _)) = ringCanCancelNegative order denomB<0 (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByPositive pRing 0<denomA b<c)))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  ... | (inl (inl 0<denomC)) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<denomC denomC<0))
+  ... | (inl (inr _)) = ringCanCancelNegative order denomB<0 (SetoidPartialOrder.<Transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByPositive pRing 0<denomA b<c)))
     where
       open Setoid S
       open Ring R
@@ -265,55 +265,55 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
       have = SetoidPartialOrder.<WellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByNegative pRing denomC<0 a<b)
   ... | inr x = exFalso (denomC!=0 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) with totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 order 0<denomB (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)) have)
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) with totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 order 0<denomB (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)) have)
     where
       open Setoid S
       open Ring R
       open Equivalence (Setoid.eq S)
       have : ((numB * denomA) * denomC) < ((numA * denomC) * denomB)
       have = SetoidPartialOrder.<WellDefined pOrder reflexive (swapLemma R) (ringCanMultiplyByPositive pRing 0<denomC a<b)
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 order denomB<0 (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 order denomB<0 (SetoidPartialOrder.<Transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)))
     where
       open Setoid S
       open Ring R
       open Equivalence (Setoid.eq S)
       have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
       have = SetoidPartialOrder.<WellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByPositive pRing 0<denomC a<b)
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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) {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 order 0<denomB (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomB
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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) {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 order 0<denomB (SetoidPartialOrder.<Transitive pOrder have (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)))
     where
       open Setoid S
       open Ring R
       open Equivalence (Setoid.eq S)
       have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
       have = SetoidPartialOrder.<WellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByNegative pRing denomC<0 a<b)
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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) {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 order denomB<0 (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)) have)
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 totality (Ring.0R R) denomC
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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) {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 order denomB<0 (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative pRing denomA<0 b<c)) have)
     where
       open Setoid S
       open Ring R
       open Equivalence (Setoid.eq S)
       have : ((numB * denomA) * denomC) < ((numA * denomC) * denomB)
       have = SetoidPartialOrder.<WellDefined pOrder reflexive (swapLemma R) (ringCanMultiplyByNegative pRing denomC<0 a<b)
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
-  SetoidPartialOrder.transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {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 (Equivalence.symmetric (Setoid.eq S) x))
+  SetoidPartialOrder.<Transitive (fieldOfFractionsOrder) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
 
   fieldOfFractionsTotalOrder : SetoidTotalOrder fieldOfFractionsOrder
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) with totality (Ring.0R R) denomA
@@ -323,26 +323,26 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) | inr x = inr (Equivalence.transitive (Setoid.eq S) x (Ring.*Commutative R))
-  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) with totality (Ring.0R R) denomA
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) with totality (numB * denomA) (numA * denomB)
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) | inr x = inr (Equivalence.symmetric (Setoid.eq S) (Equivalence.transitive (Setoid.eq S) (Ring.*Commutative R) x))
-  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inr x = exFalso (denomB!=0 (Equivalence.symmetric (Setoid.eq S) x))
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) with totality (Ring.0R R) denomB
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) with totality (Ring.0R R) denomA
-  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) with totality (numB * denomA) (numA * denomB)
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) | inr x = inr (Equivalence.transitive (Setoid.eq S) (Equivalence.symmetric (Setoid.eq S) x) (Ring.*Commutative R))
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) with totality (Ring.0R R) denomA
-  SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) with totality (numA * denomB) (numB * denomA)
   SetoidTotalOrder.totality (fieldOfFractionsTotalOrder) (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) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) | inl (inr x) = inl (inr x)
@@ -354,7 +354,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
   ineqLemma : {x y : A} → (Ring.0R R) < (x * y) → (Ring.0R R) < x → (Ring.0R R) < y
   ineqLemma {x} {y} 0<xy 0<x with totality (Ring.0R R) y
   ineqLemma {x} {y} 0<xy 0<x | inl (inl 0<y) = 0<y
-  ineqLemma {x} {y} 0<xy 0<x | inl (inr y<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<xy (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing y<0 0<x))))
+  ineqLemma {x} {y} 0<xy 0<x | inl (inr y<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<xy (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing y<0 0<x))))
     where
       open Setoid S
       open Ring R
@@ -367,7 +367,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
 
   ineqLemma' : {x y : A} → (Ring.0R R) < (x * y) → x < (Ring.0R R) → y < (Ring.0R R)
   ineqLemma' {x} {y} 0<xy x<0 with totality (Ring.0R R) y
-  ... | inl (inl 0<y) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<xy (SetoidPartialOrder.<WellDefined pOrder *Commutative (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing x<0 0<y))))
+  ... | inl (inl 0<y) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<xy (SetoidPartialOrder.<WellDefined pOrder *Commutative (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing x<0 0<y))))
     where
       open Setoid S
       open Ring R
@@ -381,7 +381,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
 
   ineqLemma'' : {x y : A} → (x * y) < (Ring.0R R) → (Ring.0R R) < x → y < (Ring.0R R)
   ineqLemma'' {x} {y} xy<0 0<x with totality (Ring.0R R) y
-  ... | inl (inl 0<y) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder xy<0 (orderRespectsMultiplication 0<x 0<y)))
+  ... | inl (inl 0<y) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder xy<0 (orderRespectsMultiplication 0<x 0<y)))
     where
       open Setoid S
       open Ring R
@@ -396,7 +396,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
   ineqLemma''' : {x y : A} → (x * y) < (Ring.0R R) → x < (Ring.0R R) → (Ring.0R R) < y
   ineqLemma''' {x} {y} xy<0 x<0 with totality (Ring.0R R) y
   ... | inl (inl 0<y) = 0<y
-  ... | inl (inr y<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder xy<0 (SetoidPartialOrder.<WellDefined pOrder (transitive *Commutative (Ring.timesZero R)) reflexive (ringCanMultiplyByNegative pRing y<0 x<0))))
+  ... | inl (inr y<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder xy<0 (SetoidPartialOrder.<WellDefined pOrder (transitive *Commutative (Ring.timesZero R)) reflexive (ringCanMultiplyByNegative pRing y<0 x<0))))
     where
       open Setoid S
       open Ring R
@@ -420,7 +420,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       0<dC : 0R < denomC
       0<dC with totality 0R denomC
       0<dC | inl (inl x) = x
-      0<dC | inl (inr dC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dBdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dC<0 0<dB))))
+      0<dC | inl (inr dC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dBdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dC<0 0<dB))))
       0<dC | inr x = exFalso (denomC!=0 (Equivalence.symmetric (Setoid.eq S) x))
       p : ((numA * denomC) * denomB) < ((numB * denomC) * denomA)
       p = SetoidPartialOrder.<WellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByPositive pRing 0<dC a<b)
@@ -433,11 +433,11 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       open Ring R
       dC<0 : denomC < 0R
       dC<0 with totality 0R denomC
-      ... | inl (inl x) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dBdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByPositive pRing x dB<0))))
+      ... | inl (inl x) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dBdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByPositive pRing x dB<0))))
       ... | inl (inr x) = x
       ... | inr x = exFalso (denomC!=0 (Equivalence.symmetric (Setoid.eq S) x))
       bad : False
-      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dAdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dC<0 0<dA)))
+      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dAdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dC<0 0<dA)))
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {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 (Equivalence.symmetric (Setoid.eq S) x))
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {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) with totality (Ring.0R R) denomB
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {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) | inl (inl 0<dB) = exFalso bad
@@ -448,15 +448,15 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       0<dC : 0R < denomC
       0<dC with totality 0R denomC
       0<dC | inl (inl x) = x
-      0<dC | inl (inr dC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dBdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dC<0 0<dB))))
+      0<dC | inl (inr dC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dBdC (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dC<0 0<dB))))
       0<dC | inr x = exFalso (denomC!=0 (Equivalence.symmetric (Setoid.eq S) x))
       dC<0 : denomC < 0R
       dC<0 with totality 0R denomC
-      dC<0 | inl (inl 0<dC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dAdC (SetoidPartialOrder.<WellDefined pOrder *Commutative (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dA<0 0<dC))))
+      dC<0 | inl (inl 0<dC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dAdC (SetoidPartialOrder.<WellDefined pOrder *Commutative (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dA<0 0<dC))))
       dC<0 | inl (inr x) = x
       dC<0 | inr x = exFalso (denomC!=0 (Equivalence.symmetric (Setoid.eq S) x))
       bad : False
-      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dC dC<0)
+      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dC dC<0)
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {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) | inl (inr dB<0) = SetoidPartialOrder.<WellDefined pOrder (symmetric *Associative) (symmetric *Associative) (ringCanMultiplyByNegative pRing dC<0 (SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric *DistributesOver+) *Commutative) (transitive (symmetric *DistributesOver+) *Commutative) have''))
     where
       open Setoid S
@@ -484,7 +484,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       dC<0 : denomC < 0R
       dC<0 = ineqLemma'' dBdC<0 0<dB
       bad : False
-      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dC dC<0)
+      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dC dC<0)
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inr dBdC<0) | inl (inl 0<dA) | inl (inr dB<0) = SetoidPartialOrder.<WellDefined pOrder (symmetric *Associative) (symmetric *Associative) (ringCanMultiplyByPositive pRing 0<dC ans)
     where
       open Setoid S
@@ -519,7 +519,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       0<dC : 0R < denomC
       0<dC = ineqLemma''' dBdC<0 dB<0
       bad : False
-      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dC dC<0)
+      bad = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dC dC<0)
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inr dBdC<0) | inl (inr dA<0) | inr x = exFalso (denomB!=0 (Equivalence.symmetric (Setoid.eq S) x))
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inr dBdC<0) | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {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 (Equivalence.symmetric (Setoid.eq S) 0=dBdC)
@@ -528,7 +528,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) with totality (Ring.0R R) (denomB * denomC)
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inl 0<dBdC) with totality (Ring.0R R) denomA
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inl 0<dBdC) | inl (inl 0<dA) with totality (Ring.0R R) denomB
-  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inl 0<dBdC) | inl (inl 0<dA) | inl (inl 0<dB) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dC dC<0))
+  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inl 0<dBdC) | inl (inl 0<dA) | inl (inl 0<dB) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dC dC<0))
     where
       open Setoid S
       open Equivalence (Setoid.eq S)
@@ -557,7 +557,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       0<dC = ineqLemma 0<dBdC 0<dB
       have : (((numB * denomA) * denomC) + ((denomA * numC) * denomB)) < (((numA * denomB) * denomC) + ((denomA * numC) * denomB))
       have = PartiallyOrderedRing.orderRespectsAddition pRing (ringCanMultiplyByPositive pRing 0<dC a<b) _
-  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inl 0<dBdC) | inl (inr dA<0) | inl (inr dB<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dC dC<0))
+  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inl 0<dBdC) | inl (inr dA<0) | inl (inr dB<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dC dC<0))
     where
       open Setoid S
       open Equivalence (Setoid.eq S)
@@ -579,7 +579,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       dC<0 = ineqLemma'' dAdC<0 0<dA
       have : (((numB * denomA) * denomC) + ((denomB * numC) * denomA)) < (((numA * denomB) * denomC) + ((denomB * numC) * denomA))
       have = PartiallyOrderedRing.orderRespectsAddition pRing (ringCanMultiplyByNegative pRing dC<0 a<b) _
-  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inr dBdC<0) | inl (inl 0<dA) | inl (inr dB<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder dC<0 0<dC))
+  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inr dBdC<0) | inl (inl 0<dA) | inl (inr dB<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder dC<0 0<dC))
     where
       open Setoid S
       open Equivalence (Setoid.eq S)
@@ -590,7 +590,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       0<dC = ineqLemma''' dBdC<0 dB<0
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inr dBdC<0) | inl (inl 0<dA) | inr x = exFalso (denomB!=0 (Equivalence.symmetric (Setoid.eq S) x))
   PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inr dBdC<0) | inl (inr dA<0) with totality (Ring.0R R) denomB
-  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inr dBdC<0) | inl (inr dA<0) | inl (inl 0<dB) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dC dC<0))
+  PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) | inl (inr dBdC<0) | inl (inr dA<0) | inl (inl 0<dB) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dC dC<0))
     where
       open Setoid S
       open Equivalence (Setoid.eq S)
@@ -631,14 +631,14 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       0<nB = SetoidPartialOrder.<WellDefined pOrder (transitive *Commutative (Ring.timesZero R)) (transitive *Commutative identIsIdent) 0<b
       0<nAnB : 0R < (numA * numB)
       0<nAnB = SetoidPartialOrder.<WellDefined pOrder (transitive *Commutative (Ring.timesZero R)) reflexive (ringCanMultiplyByPositive pRing 0<nB 0<nA)
-  PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inl 0<dAdB) | inl (inl 0<dB) | inl (inr dA<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dAdB (SetoidPartialOrder.<WellDefined pOrder *Commutative (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dA<0 0<dB))))
+  PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inl 0<dAdB) | inl (inl 0<dB) | inl (inr dA<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dAdB (SetoidPartialOrder.<WellDefined pOrder *Commutative (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dA<0 0<dB))))
     where
       open Setoid S
       open Equivalence (Setoid.eq S)
       open Ring R
   PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inl 0<dAdB) | inl (inl 0<dB) | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
   PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inl 0<dAdB) | inl (inr dB<0) with totality (Ring.0R R) denomA
-  PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inl 0<dAdB) | inl (inr dB<0) | inl (inl 0<dA) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<dAdB (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dB<0 0<dA))))
+  PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inl 0<dAdB) | inl (inr dB<0) | inl (inl 0<dA) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 0<dAdB (SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (Ring.timesZero R)) (ringCanMultiplyByNegative pRing dB<0 0<dA))))
     where
       open Setoid S
       open Equivalence (Setoid.eq S)
@@ -665,7 +665,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       open Ring R
       f : False
       f with PartiallyOrderedRing.orderRespectsMultiplication pRing 0<denomA 0<denomB
-      ... | bl = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder bl dAdB<0)
+      ... | bl = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder bl dAdB<0)
   PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inr dAdB<0) | inl (inl 0<denomB) | inl (inr denomA<0) = SetoidPartialOrder.<WellDefined pOrder (symmetric (transitive *Commutative identIsIdent)) (symmetric (transitive *Commutative (Ring.timesZero R))) ans
     where
       open Setoid S
@@ -698,13 +698,13 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
       h : 0R < (denomA * denomB)
       h = SetoidPartialOrder.<WellDefined pOrder (transitive *Commutative (Ring.timesZero R)) reflexive (ringCanMultiplyByNegative pRing denomB<0 denomA<0)
       f : False
-      f = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder dAdB<0 h)
+      f = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder dAdB<0 h)
   PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inr dAdB<0) | inl (inr denomB<0) | inr x = exFalso (denomA!=0 (Equivalence.symmetric (Setoid.eq S) x))
   PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inl (inr dAdB<0) | inr x = exFalso (denomB!=0 (Equivalence.symmetric (Setoid.eq S) x))
   PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inl 0<1) | inr 0=dAdB with IntegralDomain.intDom I (Equivalence.symmetric (Setoid.eq S) 0=dAdB)
   ... | inl x = exFalso (denomA!=0 x)
   ... | inr x = exFalso (denomB!=0 x)
-  PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inr 1<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 1<0 (SetoidPartialOrder.<WellDefined pOrder (transitive *Commutative (Ring.timesZero R)) identIsIdent (ringCanMultiplyByNegative pRing 1<0 1<0))))
+  PartiallyOrderedRing.orderRespectsMultiplication (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} 0<a 0<b | inl (inr 1<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder 1<0 (SetoidPartialOrder.<WellDefined pOrder (transitive *Commutative (Ring.timesZero R)) identIsIdent (ringCanMultiplyByNegative pRing 1<0 1<0))))
     where
       open Setoid S
       open Equivalence (Setoid.eq S)
diff --git a/KeyValue/LinearStore/Implementation.agda b/KeyValue/LinearStore/Implementation.agda
index 54c8441..9b93ce0 100644
--- a/KeyValue/LinearStore/Implementation.agda
+++ b/KeyValue/LinearStore/Implementation.agda
@@ -42,11 +42,11 @@ module KeyValue.LinearStore.Implementation where
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inl k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inr k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inr p = refl
-  lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) min<k k<min))
+  lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) with TotalOrder.totality keyOrder min k
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inl _) = lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} k v m
-  lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) min<k k<min))
+  lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inl (inr k<min) with TotalOrder.totality keyOrder k k
   lookupReducedSucceedsAfterAdd {keyOrder = keyOrder} {min} k v m | inl (inr k<min) | inl (inl k<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<k)
@@ -65,9 +65,9 @@ module KeyValue.LinearStore.Implementation where
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inl min<k') with TotalOrder.totality keyOrder min k
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr record { firstEntry = firstEntry ; next = no } () | inl (inl min<k') | inl (inl min<k)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inl (inl min<k') | inl (inl min<k) = lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {a} k' v' k v pr fst lookupReducedSucceeds
-  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) k<min (PartialOrder.transitive (TotalOrder.order keyOrder) min<k' x)))
+  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k' x)))
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr k<k') m () | inl (inl min<k') | inl (inr k<min)
-  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) x min<k'))
+  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) x min<k'))
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min v (inr x) record { firstEntry = v2 ; next = no } p | inl (inl min<k') | inr refl = applyEquality yes (yesInjective p)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} k' v' min v (inr x) record { firstEntry = .v ; next = (yes (a , b)) } refl | inl (inl min<k') | inr refl = applyEquality yes refl
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) with TotalOrder.totality keyOrder k' k
@@ -75,17 +75,17 @@ module KeyValue.LinearStore.Implementation where
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inl (inl min<k) = lookupReducedSucceeds
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m () | inl (inr k'<min) | inl (inl k'<k) | inl (inr k<min)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inr refl = lookupReducedSucceeds
-  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) x k<k'))
+  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) x k<k'))
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') with TotalOrder.totality keyOrder min k
-  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) x (PartialOrder.transitive (TotalOrder.order keyOrder) k<k' k'<min)))
+  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) x (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<k' k'<min)))
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m () | inl (inr k'<min) | inl (inr k<k') | inl (inr x)
-  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) k<k' k'<min))
+  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<k' k'<min))
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k v pr m lookupReducedSucceeds | inr refl with TotalOrder.totality keyOrder min k
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = no } () | inr refl | inl (inl min<k)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inr refl | inl (inl min<k) = lookupReducedSucceeds
-  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inr x) m lookupReducedSucceeds | inr refl | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) min<k x))
+  lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inr x) m lookupReducedSucceeds | inr refl | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k x))
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inl x) m () | inr refl | inl (inr k<min)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {k'} k' v' k v (inr x) m () | inr refl | inl (inr k<min)
   lookupReducedSucceedsAfterUnrelatedAdd {keyOrder = keyOrder} {.min} .min v' min v (inl x) m lookupReducedSucceeds | inr refl | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
@@ -116,10 +116,10 @@ module KeyValue.LinearStore.Implementation where
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inr x) record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) with TotalOrder.totality keyOrder k' k
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
-  lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) k<min min<k))
+  lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min min<k))
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inr k<min') = refl
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
-  lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) k'<k x))
+  lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k'<k x))
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inr k<k') = refl
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inl x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
   lookupReducedFailsAfterUnrelatedAdd {keyOrder = keyOrder} {min} .k v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) x)
@@ -133,13 +133,13 @@ module KeyValue.LinearStore.Implementation where
   countReducedBehavesWhenAddingNotPresent : {a b c : _} {keys : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keys} {min : keys} → (k : keys) → (v : values) → (m : ReducedMap keys values keyOrder min) → (lookupReduced {keyOrder = keyOrder} m k ≡ no) → countReduced (addReducedMap k v m) ≡ succ (countReduced m)
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v m lookupReducedFails with TotalOrder.totality keyOrder k min
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) with TotalOrder.totality keyOrder min k
-  countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) min<k k<min))
+  countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inr _) = refl
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) with TotalOrder.totality keyOrder min k
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr min<k) | inl (inl _) = refl
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr min<k) | inl (inl _) = applyEquality succ (countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} k v (_&&_.fst b) lookupReducedFails)
-  countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) min<k k<min))
+  countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inl (inr k<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) min<k k<min))
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<k)
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {min} k v m lookupReducedFails | inr refl with TotalOrder.totality keyOrder min min
   countReducedBehavesWhenAddingNotPresent {keyOrder = keyOrder} {k} k v m lookupReducedFails | inr refl | inl (inl min<min) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) min<min)
@@ -150,7 +150,7 @@ module KeyValue.LinearStore.Implementation where
   countReducedBehavesWhenAddingPresent : {a b c : _} {keys : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keys} {min : keys} → (k : keys) → (v v' : values) → (m : ReducedMap keys values keyOrder min) → (lookupReduced {keyOrder = keyOrder} m k ≡ yes v') → countReduced (addReducedMap k v m) ≡ countReduced m
   countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds with TotalOrder.totality keyOrder k min
   countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inl k<min) with TotalOrder.totality keyOrder min k
-  countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) k<min min<k))
+  countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min min<k))
   countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m () | inl (inl k<min) | inl (inr _)
   countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inr q = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (identityOfIndiscernablesLeft (TotalOrder._<_ keyOrder) k<min (equalityCommutative q)))
   countReducedBehavesWhenAddingPresent {keyOrder = keyOrder} {min} k v v' m lookupReducedSucceeds | inl (inr min<k) with TotalOrder.totality keyOrder min k
@@ -198,7 +198,7 @@ module KeyValue.LinearStore.Implementation where
 
   lookupReducedWhenLess : {a b c : _} {keyDom : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keyDom} {min : keyDom} → (m : ReducedMap keyDom values keyOrder min) → (k : keyDom) → (TotalOrder._<_ keyOrder k min) → (lookupReduced m k ≡ no)
   lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min with TotalOrder.totality keyOrder min k
-  lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) k<min min<k))
+  lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min | inl (inl min<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min min<k))
   lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min | inl (inr _) = refl
   lookupReducedWhenLess {keyOrder = keyOrder} {min} m k k<min | inr min=k rewrite min=k = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
 
@@ -220,7 +220,7 @@ module KeyValue.LinearStore.Implementation where
   lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inl min<k) = lookupCertainReduced {keyOrder = keyOrder} fst k record { index = index ; index<m = canRemoveSuccFrom<N index<m ; isHere = isHere }
   lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = zero ; index<m = _ ; isHere = isHere } | inl (inr k<min) rewrite isHere = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) k<min)
   lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) with TotalOrder.totality keyOrder a k
-  lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inl a<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) k<min (PartialOrder.transitive (TotalOrder.order keyOrder) snd a<k)))
+  lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inl a<k) = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) k<min (PartialOrder.<Transitive (TotalOrder.order keyOrder) snd a<k)))
   lookupCertainReduced {values = values} {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inr k<a) = exFalso h
     where
       f : Sg values (λ v → lookupReduced fst k ≡ yes v)
@@ -232,7 +232,7 @@ module KeyValue.LinearStore.Implementation where
       h : False
       h with f
       h | a , b rewrite g = noIsNotYes b
-  lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.transitive (TotalOrder.order keyOrder) snd k<min))
+  lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inr refl = exFalso (PartialOrder.irreflexive (TotalOrder.order keyOrder) (PartialOrder.<Transitive (TotalOrder.order keyOrder) snd k<min))
   lookupCertainReduced {keyOrder = keyOrder} {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k pr | inr min=k = firstEntry , refl
 
   lookupCertain : {a b c : _} {keyDom : Set a} {values : Set b} {keyOrder : TotalOrder {_} {c} keyDom} → (m : Map keyDom values keyOrder) → (k : keyDom) → (vecContains (keys m) k) → Sg values (λ v → lookup m k ≡ yes v)
diff --git a/Numbers/BinaryNaturals/Order.agda b/Numbers/BinaryNaturals/Order.agda
index afb46fd..7d16f42 100644
--- a/Numbers/BinaryNaturals/Order.agda
+++ b/Numbers/BinaryNaturals/Order.agda
@@ -286,18 +286,18 @@ module Numbers.BinaryNaturals.Order where
   chopDouble a b i with orderIsTotal (binNatToN a) (binNatToN b)
   chopDouble a b zero | inl (inl a<b) with orderIsTotal (2 *N binNatToN a) (2 *N binNatToN b)
   chopDouble a b zero | inl (inl a<b) | inl (inl x) = refl
-  chopDouble a b zero | inl (inl a<b) | inl (inr b<a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) b<a (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl))))
+  chopDouble a b zero | inl (inl a<b) | inl (inr b<a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) b<a (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl))))
   chopDouble a b zero | inl (inl a<b) | inr a=b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) a=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
   chopDouble a b one | inl (inl a<b) with orderIsTotal (2 *N binNatToN a) (2 *N binNatToN b)
   chopDouble a b one | inl (inl a<b) | inl (inl 2a<2b) = refl
-  chopDouble a b one | inl (inl a<b) | inl (inr 2b<2a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) a<b (cancelInequalityLeft {2} 2b<2a)))
+  chopDouble a b one | inl (inl a<b) | inl (inr 2b<2a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) a<b (cancelInequalityLeft {2} 2b<2a)))
   chopDouble a b one | inl (inl a<b) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
   chopDouble a b zero | inl (inr b<a) with orderIsTotal (2 *N binNatToN a) (2 *N binNatToN b)
-  chopDouble a b zero | inl (inr b<a) | inl (inl 2a<2b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) b<a (cancelInequalityLeft {2} {binNatToN a} {binNatToN b} 2a<2b)))
+  chopDouble a b zero | inl (inr b<a) | inl (inl 2a<2b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) b<a (cancelInequalityLeft {2} {binNatToN a} {binNatToN b} 2a<2b)))
   chopDouble a b zero | inl (inr b<a) | inl (inr 2b<2a) = refl
   chopDouble a b zero | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
   chopDouble a b one | inl (inr b<a) with orderIsTotal (2 *N binNatToN a) (2 *N binNatToN b)
-  chopDouble a b one | inl (inr b<a) | inl (inl 2a<2b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) b<a (cancelInequalityLeft {2} 2a<2b)))
+  chopDouble a b one | inl (inr b<a) | inl (inl 2a<2b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) b<a (cancelInequalityLeft {2} 2a<2b)))
   chopDouble a b one | inl (inr b<a) | inl (inr x) = refl
   chopDouble a b one | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
   chopDouble a b i | inr x with orderIsTotal (binNatToN (i :: a)) (binNatToN (i :: b))
@@ -329,19 +329,19 @@ module Numbers.BinaryNaturals.Order where
        t : a <BInherited b ≡ FirstLess
        t with orderIsTotal (binNatToN a) (binNatToN b)
        t | inl (inl x) = refl
-       t | inl (inr x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) x a<b))
+       t | inl (inr x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x a<b))
        t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
        indHyp : FirstLess ≡ go<B Equal a b
        indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
   <BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) | inl (inr b<a) = exFalso (noIntegersBetweenXAndSuccX {2 *N binNatToN a} (2 *N binNatToN b) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) 2a<2b+1)
   <BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) | inr a=b rewrite a=b | canonicalFirst a b FirstLess | canonicalSecond (canonical a) b FirstLess | transitivity (equalityCommutative (binToBin a)) (transitivity (applyEquality NToBinNat a=b) (binToBin b)) = equalityCommutative (lemma1 (canonical b))
   <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) with orderIsTotal (binNatToN a) (binNatToN b)
-  <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inl a<b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) 2b+1<2a (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) (le zero refl))))
+  <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inl a<b) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) 2b+1<2a (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) (le zero refl))))
   <BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inr b<a) = equalityCommutative (equalToFirstGreater FirstLess a b (equalityCommutative indHyp))
     where
       t : a <BInherited b ≡ FirstGreater
       t with orderIsTotal (binNatToN a) (binNatToN b)
-      t | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) x b<a))
+      t | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x b<a))
       t | inl (inr x) = refl
       t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
       indHyp : FirstGreater ≡ go<B Equal a b
@@ -354,12 +354,12 @@ module Numbers.BinaryNaturals.Order where
     where
       t : a <BInherited b ≡ FirstLess
       t with orderIsTotal (binNatToN a) (binNatToN b)
-      t | inl (inr x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) x a<b))
+      t | inl (inr x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x a<b))
       t | inl (inl x) = refl
       t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) a<b)
       indHyp : FirstLess ≡ go<B Equal a b
       indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
-  <BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inl (inr b<a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) 2a+1<2b (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) (le zero refl))))
+  <BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inl (inr b<a) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) 2a+1<2b (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) (le zero refl))))
   <BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inr a=b rewrite a=b = exFalso (succNotLess 2a+1<2b)
   <BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) with orderIsTotal (binNatToN a) (binNatToN b)
   <BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) | inl (inl a<b) = exFalso (noIntegersBetweenXAndSuccX {2 *N binNatToN b} (2 *N binNatToN a) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) 2b<2a+1)
@@ -367,7 +367,7 @@ module Numbers.BinaryNaturals.Order where
     where
       t : a <BInherited b ≡ FirstGreater
       t with orderIsTotal (binNatToN a) (binNatToN b)
-      t | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) x b<a))
+      t | inl (inl x) = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) x b<a))
       t | inl (inr x) = refl
       t | inr x rewrite x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) b<a)
       indHyp : FirstGreater ≡ go<B Equal a b
diff --git a/Numbers/BinaryNaturals/Subtraction.agda b/Numbers/BinaryNaturals/Subtraction.agda
index 3fc155a..126229e 100644
--- a/Numbers/BinaryNaturals/Subtraction.agda
+++ b/Numbers/BinaryNaturals/Subtraction.agda
@@ -138,7 +138,7 @@ module Numbers.BinaryNaturals.Subtraction where
   subLemma2 : (a b : ℕ) → a <N b → 2 *N a <N succ (2 *N b)
   subLemma2 a b a<b with TotalOrder.totality ℕTotalOrder (2 *N a) (succ (2 *N b))
   subLemma2 a b a<b | inl (inl x) = x
-  subLemma2 a b a<b | inl (inr x) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder x (TotalOrder.transitive ℕTotalOrder (lessRespectsMultiplicationLeft a b 2 a<b (le 1 refl)) (le 0 refl))))
+  subLemma2 a b a<b | inl (inr x) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder x (TotalOrder.<Transitive ℕTotalOrder (lessRespectsMultiplicationLeft a b 2 a<b (le 1 refl)) (le 0 refl))))
   subLemma2 a b a<b | inr x = exFalso (parity b a (equalityCommutative x))
 
   subtraction : (a b : BinNat) → a -B b ≡ no → binNatToN a <N binNatToN b
@@ -457,7 +457,7 @@ module Numbers.BinaryNaturals.Subtraction where
   subtraction2'' a b pr with -N pr
   subtraction2'' a b pr | record { result = result ; pr = subPr } with inspect (go zero (NToBinNat a) (NToBinNat b))
   subtraction2'' a b (inl pr) | record { result = result ; pr = subPr } | no with≡ pr2 with subtraction (NToBinNat a) (NToBinNat b) pr2
-  ... | bl rewrite nToN a | nToN b = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder pr bl))
+  ... | bl rewrite nToN a | nToN b = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder pr bl))
   subtraction2'' a b (inr pr) | record { result = result ; pr = subPr } | no with≡ pr2 with subtraction (NToBinNat a) (NToBinNat b) pr2
   ... | bl rewrite nToN a | nToN b | pr = exFalso (TotalOrder.irreflexive ℕTotalOrder bl)
   subtraction2'' a b pr | record { result = result ; pr = subPr } | yes x with≡ pr2 with subtraction2 a b pr2
diff --git a/Numbers/Integers/Order.agda b/Numbers/Integers/Order.agda
index 84cc209..00c8610 100644
--- a/Numbers/Integers/Order.agda
+++ b/Numbers/Integers/Order.agda
@@ -82,7 +82,7 @@ lessThanTotalZ {negSucc a} {negSucc .a} | inr refl = inr refl
 ℤOrder : TotalOrder ℤ
 PartialOrder._<_ (TotalOrder.order ℤOrder) = _<Z_
 PartialOrder.irreflexive (TotalOrder.order ℤOrder) {a} = irreflexive a
-PartialOrder.transitive (TotalOrder.order ℤOrder) = lessZTransitive
+PartialOrder.<Transitive (TotalOrder.order ℤOrder) = lessZTransitive
 TotalOrder.totality ℤOrder a b = lessThanTotalZ {a} {b}
 
 orderRespectsAddition : (a b : ℤ) → a <Z b → (c : ℤ) → a +Z c <Z b +Z c
diff --git a/Numbers/Modulo/IntegersModN.agda b/Numbers/Modulo/IntegersModN.agda
index 37e640f..d0d08cd 100644
--- a/Numbers/Modulo/IntegersModN.agda
+++ b/Numbers/Modulo/IntegersModN.agda
@@ -65,7 +65,7 @@ module Numbers.Modulo.IntegersModN where
   plusZnIdentityLeft {zero} {()}
   plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } with orderIsTotal x (succ n)
   plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } | inl (inl x<succn) rewrite <NRefl x<succn xLess = refl
-  plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } | inl (inr succn<x) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder succn<x xLess))
+  plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } | inl (inr succn<x) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder succn<x xLess))
   plusZnIdentityLeft {succ n} {pr} record { x = x ; xLess = xLess } | inr x=succn rewrite x=succn = exFalso (TotalOrder.irreflexive ℕTotalOrder xLess)
 
   subLemma : {a b c : ℕ} → (pr1 : a <N b) → (pr2 : a <N c) → (pr : b ≡ c) → (subtractionNResult.result (-N (inl pr1))) ≡ (subtractionNResult.result (-N (inl pr2)))
diff --git a/Numbers/Naturals/Naturals.agda b/Numbers/Naturals/Naturals.agda
index 202a000..9974d5c 100644
--- a/Numbers/Naturals/Naturals.agda
+++ b/Numbers/Naturals/Naturals.agda
@@ -541,7 +541,7 @@ module Numbers.Naturals.Naturals where
   ℕTotalOrder : TotalOrder ℕ
   PartialOrder._<_ (TotalOrder.order ℕTotalOrder) = _<N_
   PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) = lessIrreflexive
-  PartialOrder.transitive (TotalOrder.order ℕTotalOrder) = orderIsTransitive
+  PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) = orderIsTransitive
   TotalOrder.totality ℕTotalOrder = orderIsTotal
 
   doubleIsAddTwo : (a : ℕ) → a +N a ≡ 2 *N a
diff --git a/Numbers/Primes/IntegerFactorisation.agda b/Numbers/Primes/IntegerFactorisation.agda
index 2678efd..0cb4ae8 100644
--- a/Numbers/Primes/IntegerFactorisation.agda
+++ b/Numbers/Primes/IntegerFactorisation.agda
@@ -33,7 +33,7 @@ module Numbers.Primes.IntegerFactorisation where
     lemma' {a} {b} pr rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | Semiring.productZeroRight ℕSemiring a = equalityCommutative pr
 
     primeFactorisation : {p : ℕ} → (pr : Prime p) → factorisationNonunit 1 p
-    primeFactorisation {p} record { p>1 = p>1 ; pr = pr } = record {1<a = p>1 ; firstFactor = p ; firstFactorNontrivial = p>1 ; firstFactorBiggerMin = inl p>1 ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = lemma p  ; remIsSmall = zeroIsValidRem p ; quotSmall = inl (TotalOrder.transitive ℕTotalOrder (le zero refl) p>1) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = p>1 ; pr = pr} ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }
+    primeFactorisation {p} record { p>1 = p>1 ; pr = pr } = record {1<a = p>1 ; firstFactor = p ; firstFactorNontrivial = p>1 ; firstFactorBiggerMin = inl p>1 ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = lemma p  ; remIsSmall = zeroIsValidRem p ; quotSmall = inl (TotalOrder.<Transitive ℕTotalOrder (le zero refl) p>1) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = p>1 ; pr = pr} ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }
       where
         proof : (s : ℕ) → s *N 1 +N 0 ≡ s
         proof s rewrite Semiring.sumZeroRight ℕSemiring (s *N 1) | multiplicationNIsCommutative s 1 | Semiring.sumZeroRight ℕSemiring s = refl
@@ -97,9 +97,9 @@ module Numbers.Primes.IntegerFactorisation where
     factorIntegerLemma (succ zero) indHyp = inl (succPreservesInequality (succIsPositive 0))
     factorIntegerLemma (succ (succ x)) indHyp with everyNumberHasAPrimeFactor {succ (succ x)} (succPreservesInequality (succIsPositive x))
     factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = zero ; rem = .0 ; pr = ssxDivA ; remIsSmall = r } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | multiplicationNIsCommutative a 0 = exFalso (naughtE ssxDivA)
-    factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ zero ; rem = .0 ; pr = ssxDivA ; remIsSmall = r } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 1<a = succPreservesInequality (succIsPositive x) ; firstFactor = a ; firstFactorNontrivial = Prime.p>1 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = ssxDivA ; remIsSmall = r ; quotSmall = inl (TotalOrder.transitive ℕTotalOrder (le zero refl) 1<a) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }
+    factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ zero ; rem = .0 ; pr = ssxDivA ; remIsSmall = r } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 1<a = succPreservesInequality (succIsPositive x) ; firstFactor = a ; firstFactorNontrivial = Prime.p>1 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = 1 ; rem = 0 ; pr = ssxDivA ; remIsSmall = r ; quotSmall = inl (TotalOrder.<Transitive ℕTotalOrder (le zero refl) 1<a) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inl record { fst = refl ; snd = refl } ; otherFactorsNumber = 0 }
 
-    factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ (succ qu) ; rem = .0 ; pr = ssxDivA ; remIsSmall = remSmall } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 1<a = succPreservesInequality (succIsPositive x) ; firstFactor = a ; firstFactorNontrivial = Prime.p>1 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = succ (succ qu) ; rem = 0 ; pr = ssxDivA ; remIsSmall = remSmall ; quotSmall = inl (TotalOrder.transitive ℕTotalOrder (le zero refl) 1<a) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inr record {fst = succPreservesInequality (succIsPositive qu) ; snd = factNonunit} ; otherFactorsNumber = succ (factorisationNonunit.otherFactorsNumber indHypRes') }
+    factorIntegerLemma (succ (succ x)) indHyp | a , record { fst = record { fst = divides record {quot = succ (succ qu) ; rem = .0 ; pr = ssxDivA ; remIsSmall = remSmall } refl ; snd = 1<a }; snd = record { fst = primeA ; snd = smallerFactors } } = inr record { 1<a = succPreservesInequality (succIsPositive x) ; firstFactor = a ; firstFactorNontrivial = Prime.p>1 primeA ; firstFactorBiggerMin = inl (Prime.p>1 primeA) ; firstFactorDivision = record { quot = succ (succ qu) ; rem = 0 ; pr = ssxDivA ; remIsSmall = remSmall ; quotSmall = inl (TotalOrder.<Transitive ℕTotalOrder (le zero refl) 1<a) } ; firstFactorDivides = refl ; firstFactorPrime = record { p>1 = Prime.p>1 primeA ; pr = Prime.pr primeA } ; otherFactors = inr record {fst = succPreservesInequality (succIsPositive qu) ; snd = factNonunit} ; otherFactorsNumber = succ (factorisationNonunit.otherFactorsNumber indHypRes') }
       where
         indHypRes : ((succ (succ qu)) <N 2) || factorisationNonunit 1 (succ (succ qu))
         indHypRes = indHyp (succ (succ qu)) (lemma2 {a} {succ (succ qu)} {succ (succ x)} 1<a (succIsPositive (succ qu)) ssxDivA)
@@ -157,7 +157,7 @@ module Numbers.Primes.IntegerFactorisation where
             i<=firstFactor rewrite p=firstFact = firstFactorBiggerMin
             bad : False
             bad with i<=firstFactor
-            ... | inl t = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder t p<i)
+            ... | inl t = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder t p<i)
             ... | inr eq rewrite eq = TotalOrder.irreflexive ℕTotalOrder p<i
         prf zero ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inr otherFact) } p|x = zeroNeverGreater 1<a
         prf (succ x) ind record { 1<a = 1<a ; firstFactor = firstFactor ; firstFactorNontrivial = firstFactorNontrivial ; firstFactorBiggerMin = firstFactorBiggerMin ; firstFactorDivision = firstFactorDivision ; firstFactorDivides = firstFactorDivides ; firstFactorPrime = firstFactorPrime ; otherFactors = (inr otherFact) } p|x = ind (divisionAlgResult.quot firstFactorDivision) (lemma4 {divisionAlgResult.quot firstFactorDivision} {firstFactor} {divisionAlgResult.rem firstFactorDivision} {x} (divisionAlgResult.pr (firstFactorDivision)) (primesAreBiggerThanOne firstFactorPrime)) (canReduceFactorBound' (_&&_.snd otherFact) firstFactorBiggerMin) (p|q p|ffOrQ)
diff --git a/Numbers/Primes/PrimeNumbers.agda b/Numbers/Primes/PrimeNumbers.agda
index f3d5255..d480581 100644
--- a/Numbers/Primes/PrimeNumbers.agda
+++ b/Numbers/Primes/PrimeNumbers.agda
@@ -229,16 +229,16 @@ module Numbers.Primes.PrimeNumbers where
     numberLessThanOrder : (n : ℕ) → TotalOrder (numberLessThan n)
     PartialOrder._<_ (TotalOrder.order (numberLessThanOrder n)) = λ a b → (numberLessThan.a a) <N numberLessThan.a b
     PartialOrder.irreflexive (TotalOrder.order (numberLessThanOrder n)) pr = TotalOrder.irreflexive ℕTotalOrder pr
-    PartialOrder.transitive (TotalOrder.order (numberLessThanOrder n)) pr1 pr2 = orderIsTransitive pr1 pr2
+    PartialOrder.<Transitive (TotalOrder.order (numberLessThanOrder n)) pr1 pr2 = orderIsTransitive pr1 pr2
     TotalOrder.totality (numberLessThanOrder n) a b with TotalOrder.totality ℕTotalOrder (numberLessThan.a a) (numberLessThan.a b)
     TotalOrder.totality (numberLessThanOrder n) a b | inl (inl x) = inl (inl x)
     TotalOrder.totality (numberLessThanOrder n) a b | inl (inr x) = inl (inr x)
     TotalOrder.totality (numberLessThanOrder n) a b | inr x rewrite x = inr (numberLessThanEquality a b x)
 
     numberLessThanInject : {newMax : ℕ} → (max : ℕ) → (n : numberLessThan max) → (max <N newMax) → (numberLessThan newMax)
-    numberLessThanInject max record { a = n ; a<n = n<max } max<newMax = record { a = n ; a<n = PartialOrder.transitive (TotalOrder.order ℕTotalOrder) n<max max<newMax }
+    numberLessThanInject max record { a = n ; a<n = n<max } max<newMax = record { a = n ; a<n = PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) n<max max<newMax }
 
-    numberLessThanInjectComp : {max : ℕ} (a b : ℕ) → (i : numberLessThan b) → (pr : b <N a) → (pr2 : a <N max) → numberLessThanInject {max} a (numberLessThanInject {a} b i pr) pr2 ≡ numberLessThanInject {max} b i (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) pr pr2)
+    numberLessThanInjectComp : {max : ℕ} (a b : ℕ) → (i : numberLessThan b) → (pr : b <N a) → (pr2 : a <N max) → numberLessThanInject {max} a (numberLessThanInject {a} b i pr) pr2 ≡ numberLessThanInject {max} b i (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) pr pr2)
     numberLessThanInjectComp {max} a b record { a = i ; a<n = i<max } b<a a<max = numberLessThanEquality _ _ refl
 
     allNumbersLessThanDescending : (n : ℕ) → Vec (numberLessThan n) n
diff --git a/Orders.agda b/Orders.agda
index 7d6c31c..a526877 100644
--- a/Orders.agda
+++ b/Orders.agda
@@ -11,7 +11,7 @@ module Orders where
     field
       _<_ : Rel {a} {b} carrier
       irreflexive : {x : carrier} → (x < x) → False
-      transitive : {a b c : carrier} → (a < b) → (b < c) → (a < c)
+      <Transitive : {a b c : carrier} → (a < b) → (b < c) → (a < c)
 
   record TotalOrder {a b : _} (carrier : Set a) : Set (a ⊔ lsuc b) where
     field
@@ -34,12 +34,12 @@ module Orders where
     max a b | inr a=b = b
 
     irreflexive = PartialOrder.irreflexive order
-    transitive = PartialOrder.transitive order
+    <Transitive = PartialOrder.<Transitive order
 
   equivMin : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → {x y : A} → (TotalOrder._<_ order x y) → TotalOrder.min order x y ≡ x
   equivMin order {x} {y} x<y with TotalOrder.totality order x y
   equivMin order {x} {y} x<y | inl (inl x₁) = refl
-  equivMin order {x} {y} x<y | inl (inr y<x) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.transitive (TotalOrder.order order) x<y y<x))
+  equivMin order {x} {y} x<y | inl (inr y<x) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) x<y y<x))
   equivMin order {x} {y} x<y | inr x=y rewrite x=y = refl
 
   equivMin' : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → {x y : A} → (TotalOrder.min order x y ≡ x) → (TotalOrder._<_ order x y) || (x ≡ y)
@@ -51,12 +51,12 @@ module Orders where
   minCommutes : {a b : _} {A : Set a} → (order : TotalOrder {a} {b} A) → (x y : A) → (TotalOrder.min order x y) ≡ (TotalOrder.min order y x)
   minCommutes order x y with TotalOrder.totality order x y
   minCommutes order x y | inl (inl x<y) with TotalOrder.totality order y x
-  minCommutes order x y | inl (inl x<y) | inl (inl y<x) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.transitive (TotalOrder.order order) y<x x<y))
+  minCommutes order x y | inl (inl x<y) | inl (inl y<x) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<x x<y))
   minCommutes order x y | inl (inl x<y) | inl (inr x<y') = refl
   minCommutes order x y | inl (inl x<y) | inr y=x = equalityCommutative y=x
   minCommutes order x y | inl (inr y<x) with TotalOrder.totality order y x
   minCommutes order x y | inl (inr y<x) | inl (inl y<x') = refl
-  minCommutes order x y | inl (inr y<x) | inl (inr x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.transitive (TotalOrder.order order) y<x x<y))
+  minCommutes order x y | inl (inr y<x) | inl (inr x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<x x<y))
   minCommutes order x y | inl (inr y<x) | inr y=x = refl
   minCommutes order x y | inr x=y with TotalOrder.totality order y x
   minCommutes order x y | inr x=y | inl (inl x₁) = x=y
@@ -74,14 +74,14 @@ module Orders where
   swapMin {order = order} {x} {y} {z} | inl (inl y<z) with TotalOrder.totality order x z
   swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inl x<z) = minCommutes order x y
   swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) with TotalOrder.totality order x y
-  swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inl (inl x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.transitive (TotalOrder.order order) y<z (PartialOrder.transitive (TotalOrder.order order) z<x x<y)))
+  swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inl (inl x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<z (PartialOrder.<Transitive (TotalOrder.order order) z<x x<y)))
   swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inl (inr y<x) = equalityCommutative (equivMin order y<z)
   swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inl (inr z<x) | inr x=y rewrite x=y = equalityCommutative (equivMin order y<z)
   swapMin {order = order} {x} {y} {z} | inl (inl y<z) | inr x=z = minCommutes order x y
   swapMin {order = order} {x} {y} {z} | inl (inr z<y) with TotalOrder.totality order x z
-  swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inl x<z) rewrite minCommutes order y x = equalityCommutative (equivMin order (PartialOrder.transitive (TotalOrder.order order) x<z z<y))
+  swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inl x<z) rewrite minCommutes order y x = equalityCommutative (equivMin order (PartialOrder.<Transitive (TotalOrder.order order) x<z z<y))
   swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) with TotalOrder.totality order y z
-  swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inl (inl y<z) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.transitive (TotalOrder.order order) z<y y<z))
+  swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inl (inl y<z) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) z<y y<z))
   swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inl (inr z<y') = refl
   swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inl (inr z<x) | inr y=z = equalityCommutative y=z
   swapMin {order = order} {x} {y} {z} | inl (inr z<y) | inr x=z rewrite x=z | minCommutes order y z = equalityCommutative (equivMin order z<y)
@@ -94,7 +94,7 @@ module Orders where
   minMin order {x} {y} with TotalOrder.totality order x y
   minMin order {x} {y} | inl (inl x<y) = minIdempotent order x
   minMin order {x} {y} | inl (inr y<x) with TotalOrder.totality order x y
-  minMin order {x} {y} | inl (inr y<x) | inl (inl x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.transitive (TotalOrder.order order) y<x x<y))
+  minMin order {x} {y} | inl (inr y<x) | inl (inl x<y) = exFalso (PartialOrder.irreflexive (TotalOrder.order order) (PartialOrder.<Transitive (TotalOrder.order order) y<x x<y))
   minMin order {x} {y} | inl (inr y<x) | inl (inr y<x') = refl
   minMin order {x} {y} | inl (inr y<x) | inr x=y = x=y
   minMin order {x} {y} | inr x=y = minIdempotent order x
diff --git a/Rings/Orders/Partial/Lemmas.agda b/Rings/Orders/Partial/Lemmas.agda
index 9984e8e..fa1b26e 100644
--- a/Rings/Orders/Partial/Lemmas.agda
+++ b/Rings/Orders/Partial/Lemmas.agda
@@ -27,7 +27,7 @@ abstract
   open import Rings.Lemmas R
 
   ringAddInequalities : {w x y z : A} → w < x → y < z → (w + y) < (x + z)
-  ringAddInequalities {w = w} {x} {y} {z} w<x y<z = transitive (orderRespectsAddition w<x y) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition y<z x))
+  ringAddInequalities {w = w} {x} {y} {z} w<x y<z = <Transitive (orderRespectsAddition w<x y) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition y<z x))
 
   ringCanMultiplyByPositive : {x y c : A} → (Ring.0R R) < c → x < y → (x * c) < (y * c)
   ringCanMultiplyByPositive {x} {y} {c} 0<c x<y = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.identRight additiveGroup) q'
@@ -45,7 +45,7 @@ abstract
       q' = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup))) q
 
   ringMultiplyPositives : {x y a b : A} → 0R < x → 0R < a → (x < y) → (a < b) → (x * a) < (y * b)
-  ringMultiplyPositives {x} {y} {a} {b} 0<x 0<a x<y a<b = SetoidPartialOrder.transitive pOrder (ringCanMultiplyByPositive 0<a x<y) (<WellDefined *Commutative *Commutative (ringCanMultiplyByPositive (SetoidPartialOrder.transitive pOrder 0<x x<y) a<b))
+  ringMultiplyPositives {x} {y} {a} {b} 0<x 0<a x<y a<b = SetoidPartialOrder.<Transitive pOrder (ringCanMultiplyByPositive 0<a x<y) (<WellDefined *Commutative *Commutative (ringCanMultiplyByPositive (SetoidPartialOrder.<Transitive pOrder 0<x x<y) a<b))
 
   ringSwapNegatives : {x y : A} → (Group.inverse (Ring.additiveGroup R) x) < (Group.inverse (Ring.additiveGroup R) y) → y < x
   ringSwapNegatives {x} {y} -x<-y = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) (Group.identLeft additiveGroup) v
diff --git a/Rings/Orders/Total/Lemmas.agda b/Rings/Orders/Total/Lemmas.agda
index ec48038..0bfd458 100644
--- a/Rings/Orders/Total/Lemmas.agda
+++ b/Rings/Orders/Total/Lemmas.agda
@@ -38,10 +38,10 @@ abstract
   absWellDefined a b a=b with totality 0R a
   absWellDefined a b a=b | inl (inl 0<a) with totality 0R b
   absWellDefined a b a=b | inl (inl 0<a) | inl (inl 0<b) = a=b
-  absWellDefined a b a=b | inl (inl 0<a) | inl (inr b<0) = exFalso (irreflexive {0G} (transitive 0<a (<WellDefined (Equivalence.symmetric eq a=b) (Equivalence.reflexive eq) b<0)))
+  absWellDefined a b a=b | inl (inl 0<a) | inl (inr b<0) = exFalso (irreflexive {0G} (<Transitive 0<a (<WellDefined (Equivalence.symmetric eq a=b) (Equivalence.reflexive eq) b<0)))
   absWellDefined a b a=b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) 0<a))
   absWellDefined a b a=b | inl (inr a<0) with totality 0R b
-  absWellDefined a b a=b | inl (inr a<0) | inl (inl 0<b) = exFalso (irreflexive {0G} (transitive 0<b (<WellDefined a=b (Equivalence.reflexive eq) a<0)))
+  absWellDefined a b a=b | inl (inr a<0) | inl (inl 0<b) = exFalso (irreflexive {0G} (<Transitive 0<b (<WellDefined a=b (Equivalence.reflexive eq) a<0)))
   absWellDefined a b a=b | inl (inr a<0) | inl (inr b<0) = inverseWellDefined additiveGroup a=b
   absWellDefined a b a=b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) (Equivalence.reflexive eq) a<0))
   absWellDefined a b a=b | inr 0=a with totality 0R b
@@ -52,7 +52,7 @@ abstract
   lemm2 : (a : A) → a < 0G → 0G < inverse a
   lemm2 a a<0 with totality 0R (inverse a)
   lemm2 a a<0 | inl (inl 0<-a) = 0<-a
-  lemm2 a a<0 | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (invLeft {a}) (identLeft {a}) (orderRespectsAddition -a<0 a)) a<0))
+  lemm2 a a<0 | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (invLeft {a}) (identLeft {a}) (orderRespectsAddition -a<0 a)) a<0))
   lemm2 a a<0 | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) (Equivalence.reflexive eq) a<0))
     where
       t : a + 0G ∼ 0G
@@ -60,7 +60,7 @@ abstract
 
   lemm2' : (a : A) → 0G < a → inverse a < 0G
   lemm2' a 0<a with totality 0R (inverse a)
-  lemm2' a 0<a | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a (<WellDefined (identLeft {a}) (invLeft {a}) (orderRespectsAddition 0<-a a))))
+  lemm2' a 0<a | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<a (<WellDefined (identLeft {a}) (invLeft {a}) (orderRespectsAddition 0<-a a))))
   lemm2' a 0<a | inl (inr -a<0) = -a<0
   lemm2' a 0<a | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) 0<a))
     where
@@ -72,36 +72,36 @@ abstract
   triangleInequality a b | inl (inl 0<a+b) with totality 0R a
   triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) with totality 0R b
   triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inl 0<b) = inr (Equivalence.reflexive eq)
-  triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 b b<0)) a))
+  triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder b<0 (lemm2 b b<0)) a))
   triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inr 0=b = inr (Equivalence.reflexive eq)
   triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) with totality 0R b
-  triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 a a<0)) b)
-  triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a+b (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities a<0 b<0))))
-  triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inr 0=b = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 a a<0)) b)
+  triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder a<0 (lemm2 a a<0)) b)
+  triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<a+b (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities a<0 b<0))))
+  triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inr 0=b = inl (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder a<0 (lemm2 a a<0)) b)
   triangleInequality a b | inl (inl 0<a+b) | inr 0=a with totality 0R b
   triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inl 0<b) = inr (Equivalence.reflexive eq)
-  triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 b b<0)) a))
+  triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder b<0 (lemm2 b b<0)) a))
   triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inr 0=b = inr (Equivalence.reflexive eq)
   triangleInequality a b | inl (inr a+b<0) with totality 0G a
   triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) with totality 0G b
-  triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<a 0<b)) a+b<0))
-  triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (invContravariant additiveGroup)) (inverseWellDefined additiveGroup groupIsAbelian)) (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.transitive pOrder (lemm2' _ 0<a) 0<a) (inverse b)))
-  triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) identRight) (Equivalence.reflexive eq) a+b<0)))
+  triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<a 0<b)) a+b<0))
+  triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (invContravariant additiveGroup)) (inverseWellDefined additiveGroup groupIsAbelian)) (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder (lemm2' _ 0<a) 0<a) (inverse b)))
+  triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<a (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) identRight) (Equivalence.reflexive eq) a+b<0)))
   triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) with totality 0G b
-  triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inl 0<b) = inl (<WellDefined (Equivalence.symmetric eq (invContravariant additiveGroup)) groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder (lemm2' _ 0<b) 0<b) (inverse a)))
+  triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inl 0<b) = inl (<WellDefined (Equivalence.symmetric eq (invContravariant additiveGroup)) groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder (lemm2' _ 0<b) 0<b) (inverse a)))
   triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian)
   triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inr 0=b = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=b)) (invIdentity additiveGroup)) (Equivalence.reflexive eq)) identLeft) (Equivalence.symmetric eq identRight)) (+WellDefined (Equivalence.reflexive eq) 0=b)))
   triangleInequality a b | inl (inr a+b<0) | inr 0=a with totality 0G b
-  triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<b (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) identLeft) (Equivalence.reflexive eq) a+b<0)))
+  triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<b (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) identLeft) (Equivalence.reflexive eq) a+b<0)))
   triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (inverseWellDefined additiveGroup 0=a)) (invIdentity additiveGroup)) 0=a) (Equivalence.reflexive eq))))
   triangleInequality a b | inl (inr a+b<0) | inr 0=a | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.symmetric eq 0=b)) identLeft) (Equivalence.reflexive eq) a+b<0))
   triangleInequality a b | inr 0=a+b with totality 0G a
   triangleInequality a b | inr 0=a+b | inl (inl 0<a) with totality 0G b
   triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined identLeft (Equivalence.symmetric eq 0=a+b) (ringAddInequalities 0<a 0<b)))
-  triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 _ b<0)) a))
+  triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder b<0 (lemm2 _ b<0)) a))
   triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) 0<a))
   triangleInequality a b | inr 0=a+b | inl (inr a<0) with totality 0G b
-  triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 _ a<0)) b)
+  triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder a<0 (lemm2 _ a<0)) b)
   triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=a+b) identLeft (ringAddInequalities a<0 b<0)))
   triangleInequality a b | inr 0=a+b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) (Equivalence.reflexive eq) a<0))
   triangleInequality a b | inr 0=a+b | inr 0=a with totality 0G b
@@ -188,7 +188,7 @@ abstract
       p2 = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq (Group.+WellDefined additiveGroup *Commutative *Commutative) (Equivalence.transitive eq (symmetric *DistributesOver+) *Commutative)) p1
       q : (y + inverse x) < 0R
       q with totality 0R (y + inverse x)
-      q | inl (inl pr) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder bad c<0))
+      q | inl (inl pr) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<Transitive pOrder bad c<0))
         where
           bad : 0R < c
           bad = ringCanCancelPositive pr (SetoidPartialOrder.<WellDefined pOrder (symmetric (Equivalence.transitive eq *Commutative (Ring.timesZero R))) *Commutative p2)
@@ -209,12 +209,12 @@ abstract
   absNegation : (a : A) → (abs a) ∼ (abs (inverse a))
   absNegation a with totality 0R a
   absNegation a | inl (inl 0<a) with totality 0G (inverse a)
-  absNegation a | inl (inl 0<a) | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<-a (lemm2' a 0<a)))
+  absNegation a | inl (inl 0<a) | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<-a (lemm2' a 0<a)))
   absNegation a | inl (inl 0<a) | inl (inr -a<0) = Equivalence.symmetric eq (invTwice additiveGroup a)
   absNegation a | inl (inl 0<a) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invTwice additiveGroup a)) (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=-a))) (invIdent additiveGroup)) 0<a))
   absNegation a | inl (inr a<0) with totality 0G (inverse a)
   absNegation a | inl (inr a<0) | inl (inl 0<-a) = Equivalence.reflexive eq
-  absNegation a | inl (inr a<0) | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) -a<0)) a<0))
+  absNegation a | inl (inr a<0) | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) -a<0)) a<0))
   absNegation a | inl (inr a<0) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq (inverseWellDefined additiveGroup 0=-a) (invTwice additiveGroup a))) (invIdent additiveGroup)) (Equivalence.reflexive eq) a<0))
   absNegation a | inr 0=a with totality 0G (inverse a)
   absNegation a | inr 0=a | inl (inl 0<-a) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=a)) (invIdent additiveGroup)) 0<-a))
@@ -234,11 +234,11 @@ abstract
   absRespectsTimes a b | inl (inl 0<a) with totality 0R b
   absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) with totality 0R (a * b)
   absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inl 0<ab) = Equivalence.reflexive eq
-  absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (orderRespectsMultiplication 0<a 0<b) ab<0))
+  absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (orderRespectsMultiplication 0<a 0<b) ab<0))
   absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (orderRespectsMultiplication 0<a 0<b)))
   absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) with totality 0R (a * b)
   absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inl 0<ab) with <WellDefined (Equivalence.reflexive eq) ringMinusExtracts (orderRespectsMultiplication 0<a (lemm2 b b<0))
-  ... | bl = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<ab (<WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ bl))))
+  ... | bl = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<ab (<WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ bl))))
   absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts
   absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=ab) (Equivalence.reflexive eq) (posTimesNeg a b 0<a b<0)))
   absRespectsTimes a b | inl (inl 0<a) | inr 0=b with totality 0R (a * b)
@@ -247,12 +247,12 @@ abstract
   absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inr 0=ab = Equivalence.reflexive eq
   absRespectsTimes a b | inl (inr a<0) with totality 0R b
   absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) with totality 0R (a * b)
-  absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inl 0<ab) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<ab (<WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0))))
+  absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inl 0<ab) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<ab (<WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0))))
   absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts'
   absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq 0=ab *Commutative)) (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0)))
   absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) with totality 0R (a * b)
   absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inl 0<ab) = Equivalence.symmetric eq twoNegativesTimes
-  absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (negTimesPos a b a<0 b<0) ab<0))
+  absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (negTimesPos a b a<0 b<0) ab<0))
   absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inr 0=ab = exFalso (exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (negTimesPos a b a<0 b<0))))
   absRespectsTimes a b | inl (inr a<0) | inr 0=b with totality 0R (a * b)
   absRespectsTimes a b | inl (inr a<0) | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) 0<ab))
@@ -274,8 +274,8 @@ abstract
 
   absNonnegative : {a : A} → (abs a < 0R) → False
   absNonnegative {a} pr with totality 0R a
-  absNonnegative {a} pr | inl (inl x) = irreflexive {0G} (SetoidPartialOrder.transitive pOrder x pr)
-  absNonnegative {a} pr | inl (inr x) = irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) pr)) x)
+  absNonnegative {a} pr | inl (inl x) = irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder x pr)
+  absNonnegative {a} pr | inl (inr x) = irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) pr)) x)
   absNonnegative {a} pr | inr x = irreflexive {0G} (<WellDefined (Equivalence.symmetric eq x) (Equivalence.reflexive eq) pr)
 
   a-bPos : {a b : A} → ((a ∼ b) → False) → 0R < abs (a + inverse b)
@@ -293,7 +293,7 @@ abstract
   halvePositive : (a : A) → 0R < (a + a) → 0R < a
   halvePositive a 0<2a with totality 0R a
   halvePositive a 0<2a | inl (inl x) = x
-  halvePositive a 0<2a | inl (inr a<0) = exFalso (irreflexive {a + a} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) identRight (ringAddInequalities a<0 a<0)) 0<2a))
+  halvePositive a 0<2a | inl (inr a<0) = exFalso (irreflexive {a + a} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) identRight (ringAddInequalities a<0 a<0)) 0<2a))
   halvePositive a 0<2a | inr x = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq x) (Equivalence.symmetric eq x)) identRight) 0<2a))
 
   0<1 : (0R ∼ 1R → False) → 0R < 1R
@@ -310,18 +310,18 @@ abstract
 
   1<0False : (1R < 0R) → False
   1<0False 1<0 with orderRespectsMultiplication (lemm2 _ 1<0) (lemm2 _ 1<0)
-  ... | bl = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 1<0 (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (twoNegativesTimes) identIsIdent) bl)))
+  ... | bl = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 1<0 (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (twoNegativesTimes) identIsIdent) bl)))
 
   greaterZeroImpliesEqualAbs : {a : A} → 0R < a → a ∼ abs a
   greaterZeroImpliesEqualAbs {a} 0<a with totality 0R a
   ... | inl (inl _) = Equivalence.reflexive eq
-  ... | inl (inr a<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder a<0 0<a))
+  ... | inl (inr a<0) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder a<0 0<a))
   ... | inr 0=a = exFalso (irreflexive (<WellDefined 0=a (Equivalence.reflexive eq) 0<a))
 
   lessZeroImpliesEqualNegAbs : {a : A} → a < 0R → abs a ∼ inverse a
   lessZeroImpliesEqualNegAbs {a} a<0 with totality 0R a
   ... | inl (inr _) = Equivalence.reflexive eq
-  ... | inl (inl 0<a) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder a<0 0<a))
+  ... | inl (inl 0<a) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder a<0 0<a))
   ... | inr 0=a = exFalso (irreflexive (<WellDefined (Equivalence.reflexive eq) 0=a a<0))
 
   absZeroIsZero : abs 0R ∼ 0R
@@ -332,8 +332,8 @@ abstract
 
   greaterThanAbsImpliesGreaterThan0 : {a b : A} → (abs a) < b → 0R < b
   greaterThanAbsImpliesGreaterThan0 {a} {b} a<b with totality 0R a
-  greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inl 0<a) = SetoidPartialOrder.transitive pOrder 0<a a<b
-  greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inr a<0) = SetoidPartialOrder.transitive pOrder (lemm2 _ a<0) a<b
+  greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inl 0<a) = SetoidPartialOrder.<Transitive pOrder 0<a a<b
+  greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inr a<0) = SetoidPartialOrder.<Transitive pOrder (lemm2 _ a<0) a<b
   greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inr 0=a = <WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq) a<b
 
   abs1Is1 : abs 1R ∼ 1R
@@ -345,5 +345,5 @@ abstract
   absBoundedImpliesBounded : {a b : A} → abs a < b → a < b
   absBoundedImpliesBounded {a} {b} a<b with totality 0G a
   absBoundedImpliesBounded {a} {b} a<b | inl (inl x) = a<b
-  absBoundedImpliesBounded {a} {b} a<b | inl (inr x) = SetoidPartialOrder.transitive pOrder x (SetoidPartialOrder.transitive pOrder (lemm2 a x) a<b)
+  absBoundedImpliesBounded {a} {b} a<b | inl (inr x) = SetoidPartialOrder.<Transitive pOrder x (SetoidPartialOrder.<Transitive pOrder (lemm2 a x) a<b)
   absBoundedImpliesBounded {a} {b} a<b | inr x = a<b
diff --git a/Setoids/Orders.agda b/Setoids/Orders.agda
index 5564e0f..33cc720 100644
--- a/Setoids/Orders.agda
+++ b/Setoids/Orders.agda
@@ -14,7 +14,7 @@ record SetoidPartialOrder {a b c : _} {A : Set a} (S : Setoid {a} {b} A) (_<_ :
   field
     <WellDefined : {a b c d : A} → (a ∼ b) → (c ∼ d) → a < c → b < d
     irreflexive : {x : A} → (x < x) → False
-    transitive : {a b c : A} → (a < b) → (b < c) → (a < c)
+    <Transitive : {a b c : A} → (a < b) → (b < c) → (a < c)
 
 record SetoidTotalOrder {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {a} {c} A} (P : SetoidPartialOrder S _<_) : Set (a ⊔ b ⊔ c) where
   open Setoid S
@@ -36,7 +36,7 @@ record SetoidTotalOrder {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Re
 partialOrderToSetoidPartialOrder : {a b : _} {A : Set a} (P : PartialOrder {a} {b} A) → SetoidPartialOrder (reflSetoid A) (PartialOrder._<_ P)
 SetoidPartialOrder.<WellDefined (partialOrderToSetoidPartialOrder P) a=b c=d a<c rewrite a=b | c=d = a<c
 SetoidPartialOrder.irreflexive (partialOrderToSetoidPartialOrder P) = PartialOrder.irreflexive P
-SetoidPartialOrder.transitive (partialOrderToSetoidPartialOrder P) = PartialOrder.transitive P
+SetoidPartialOrder.<Transitive (partialOrderToSetoidPartialOrder P) = PartialOrder.<Transitive P
 
 totalOrderToSetoidTotalOrder : {a b : _} {A : Set a} (T : TotalOrder {a} {b} A) → SetoidTotalOrder (partialOrderToSetoidPartialOrder (TotalOrder.order T))
 SetoidTotalOrder.totality (totalOrderToSetoidTotalOrder T) = TotalOrder.totality T
diff --git a/Sets/CantorBijection/Order.agda b/Sets/CantorBijection/Order.agda
index 723e710..c8fa1a0 100644
--- a/Sets/CantorBijection/Order.agda
+++ b/Sets/CantorBijection/Order.agda
@@ -19,10 +19,10 @@ totalOrder : TotalOrder (ℕ && ℕ)
 PartialOrder._<_ (TotalOrder.order totalOrder) = order
 PartialOrder.irreflexive (TotalOrder.order totalOrder) {fst ,, snd} (inl x) = exFalso (TotalOrder.irreflexive ℕTotalOrder x)
 PartialOrder.irreflexive (TotalOrder.order totalOrder) {fst ,, snd} (inr (_ ,, p)) = exFalso (TotalOrder.irreflexive ℕTotalOrder p)
-PartialOrder.transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inl pr1) (inl pr2) = inl (TotalOrder.transitive ℕTotalOrder pr1 pr2)
-PartialOrder.transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inl pr1) (inr (f1 ,, f2)) = inl (identityOfIndiscernablesRight _<N_ pr1 f1)
-PartialOrder.transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inr (f1 ,, f2)) (inl x) = inl (identityOfIndiscernablesLeft _<N_ x (equalityCommutative f1))
-PartialOrder.transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inr (f1 ,, f2)) (inr (fst ,, snd)) = inr (transitivity f1 fst ,, TotalOrder.transitive ℕTotalOrder f2 snd)
+PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inl pr1) (inl pr2) = inl (TotalOrder.<Transitive ℕTotalOrder pr1 pr2)
+PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inl pr1) (inr (f1 ,, f2)) = inl (identityOfIndiscernablesRight _<N_ pr1 f1)
+PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inr (f1 ,, f2)) (inl x) = inl (identityOfIndiscernablesLeft _<N_ x (equalityCommutative f1))
+PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inr (f1 ,, f2)) (inr (fst ,, snd)) = inr (transitivity f1 fst ,, TotalOrder.<Transitive ℕTotalOrder f2 snd)
 TotalOrder.totality totalOrder (a ,, b) (c ,, d) with TotalOrder.totality ℕTotalOrder (a +N b) (c +N d)
 TotalOrder.totality totalOrder (a ,, b) (c ,, d) | inl (inl x) = inl (inl (inl x))
 TotalOrder.totality totalOrder (a ,, b) (c ,, d) | inl (inr x) = inl (inr (inl x))
@@ -83,7 +83,7 @@ orderWellfounded (a ,, b) = access (go b a)
           where
             bad : (x y1 y2 : ℕ) → y1 +N y2 ≡ x → x <N y2 → False
             bad x zero y2 y1+y2=x x<y2 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x<y2 y1+y2=x)
-            bad x (succ y1) y2 y1+y2=x x<y2 rewrite equalityCommutative y1+y2=x = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder x<y2 (identityOfIndiscernablesRight _<N_ (addingIncreases y2 y1) (Semiring.commutative ℕSemiring y2 (succ y1))))
+            bad x (succ y1) y2 y1+y2=x x<y2 rewrite equalityCommutative y1+y2=x = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder x<y2 (identityOfIndiscernablesRight _<N_ (addingIncreases y2 y1) (Semiring.commutative ℕSemiring y2 (succ y1))))
         ans (succ fst ,, snd) (inr (a1 ,, a2)) rewrite y1+y2=x = inr (a1 ,, le fst a1)
     g (succ x) pr zero (zero ,, y2) (inr (fst ,, snd)) = exFalso (TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _<N_ snd fst))
     g (succ x) pr zero (succ y1 ,, y2) (inr (fst ,, snd)) = pr y2 snd (succ (succ y1)) (succ y1 ,, y2) (inl (le 0 refl))
diff --git a/Sets/CantorBijection/Proofs.agda b/Sets/CantorBijection/Proofs.agda
index 8dd0a34..05c58de 100644
--- a/Sets/CantorBijection/Proofs.agda
+++ b/Sets/CantorBijection/Proofs.agda
@@ -64,7 +64,7 @@ module Sets.CantorBijection.Proofs where
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, zero | inl (inr pr1) rewrite Semiring.commutative ℕSemiring y1 1 = exFalso (zeroNeverGreater (canRemoveSuccFrom<N pr1))
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, zero | inr pr1 = inr (pr1 ,, le 0 refl)
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, zero | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring y1 (succ (succ y2)) = inl (succPreservesInequality (succIsPositive (y2 +N y1)))
-  cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, zero | zero ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.sumZeroRight ℕSemiring y2 | Semiring.sumZeroRight ℕSemiring x1 = inl (TotalOrder.transitive ℕTotalOrder pr (a<SuccA _))
+  cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, zero | zero ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.sumZeroRight ℕSemiring y2 | Semiring.sumZeroRight ℕSemiring x1 = inl (TotalOrder.<Transitive ℕTotalOrder pr (a<SuccA _))
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, zero | succ y1 ,, zero rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.commutative ℕSemiring y1 1 | Semiring.sumZeroRight ℕSemiring x1 | Semiring.sumZeroRight ℕSemiring y1 = inl pr
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, zero | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.sumZeroRight ℕSemiring x1 = inl (identityOfIndiscernablesRight _<N_ pr (transitivity (applyEquality succ (Semiring.commutative ℕSemiring y1 (succ y2))) (Semiring.commutative ℕSemiring (succ (succ y2)) y1)))
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | zero ,, succ x2 | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring x2 | Semiring.sumZeroRight ℕSemiring y2 = inl (succPreservesInequality pr)
@@ -82,7 +82,7 @@ module Sets.CantorBijection.Proofs where
       ans | inl (inl x) = inl x
       ans | inl (inr x) = exFalso (noIntegersBetweenXAndSuccX (succ x2) pr (identityOfIndiscernablesLeft _<N_ x (transitivity (Semiring.commutative ℕSemiring y1 (succ (succ y2))) (applyEquality succ (Semiring.commutative ℕSemiring (succ y2) y1)))))
       ans | inr x = inr (x ,, succIsPositive (succ y2))
-  cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, succ x2 | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring y2 = inl (TotalOrder.transitive ℕTotalOrder (identityOfIndiscernablesLeft _<N_ pr (transitivity (applyEquality succ (Semiring.commutative ℕSemiring x1 (succ x2))) (Semiring.commutative ℕSemiring (succ (succ x2)) x1))) (a<SuccA (succ y2)))
+  cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, succ x2 | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring y2 = inl (TotalOrder.<Transitive ℕTotalOrder (identityOfIndiscernablesLeft _<N_ pr (transitivity (applyEquality succ (Semiring.commutative ℕSemiring x1 (succ x2))) (Semiring.commutative ℕSemiring (succ (succ x2)) x1))) (a<SuccA (succ y2)))
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, succ x2 | succ y1 ,, zero rewrite Semiring.commutative ℕSemiring y1 1 | Semiring.sumZeroRight ℕSemiring y1 | Semiring.commutative ℕSemiring x1 (succ x2) | Semiring.commutative ℕSemiring x1 (succ (succ x2)) = inl pr
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inl pr | succ x1 ,, succ x2 | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 (succ x2) | Semiring.commutative ℕSemiring y1 (succ y2) | Semiring.commutative ℕSemiring x1 (succ (succ x2)) | Semiring.commutative ℕSemiring y1 (succ (succ y2)) = inl pr
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) with cantorInverse x
@@ -90,7 +90,7 @@ module Sets.CantorBijection.Proofs where
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, ()) | zero ,, zero | zero ,, zero
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (() ,, snd) | zero ,, zero | zero ,, succ y2
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (refl ,, snd) | zero ,, succ .y2 | zero ,, succ y2 = exFalso (TotalOrder.irreflexive ℕTotalOrder snd)
-  cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (refl ,, snd) | zero ,, succ .(y1 +N succ y2) | succ y1 ,, succ y2 = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder snd (identityOfIndiscernablesRight _<N_ (addingIncreases (succ y2) y1) (Semiring.commutative ℕSemiring (succ y2) (succ y1)))))
+  cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (refl ,, snd) | zero ,, succ .(y1 +N succ y2) | succ y1 ,, succ y2 = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder snd (identityOfIndiscernablesRight _<N_ (addingIncreases (succ y2) y1) (Semiring.commutative ℕSemiring (succ y2) (succ y1)))))
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | succ x1 ,, zero | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring x1 | succInjective fst | Semiring.commutative ℕSemiring y2 1 | Semiring.sumZeroRight ℕSemiring y2 = inl (le zero refl)
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | succ x1 ,, zero | succ y1 ,, succ y2 rewrite Semiring.commutative ℕSemiring x1 1 | Semiring.sumZeroRight ℕSemiring x1 = inr (transitivity fst (transitivity (applyEquality succ (Semiring.commutative ℕSemiring y1 (succ y2))) (Semiring.commutative ℕSemiring (succ (succ y2)) y1)) ,, succPreservesInequality snd)
   cantorInverseOrderPreserving (succ x) (succ y) x<y | inr (fst ,, snd) | succ x1 ,, succ x2 | zero ,, succ y2 rewrite Semiring.sumZeroRight ℕSemiring y2 | Semiring.commutative ℕSemiring x1 (succ x2) | Semiring.commutative ℕSemiring (succ (succ x2)) x1 | fst = inl (succPreservesInequality (le zero refl))
@@ -117,7 +117,7 @@ module Sets.CantorBijection.Proofs where
   cantorInverseDiscrete (succ a) (succ b ,, c) a<c (inl x) | zero ,, zero = zeroNeverGreater (canRemoveSuccFrom<N x)
   cantorInverseDiscrete (succ a) (b ,, zero) (inl x) (inr (fst ,, snd)) | zero ,, zero = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x fst)
   cantorInverseDiscrete (succ a) (b ,, succ c) a<c (inr (fst ,, snd)) | zero ,, zero = zeroNeverGreater (canRemoveSuccFrom<N snd)
-  cantorInverseDiscrete (succ a) (b ,, c) (inl y) (inl x) | zero ,, succ snd rewrite Semiring.commutative ℕSemiring snd 1 | Semiring.sumZeroRight ℕSemiring snd = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder x y)
+  cantorInverseDiscrete (succ a) (b ,, c) (inl y) (inl x) | zero ,, succ snd rewrite Semiring.commutative ℕSemiring snd 1 | Semiring.sumZeroRight ℕSemiring snd = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder x y)
   cantorInverseDiscrete (succ a) (b ,, succ c) (inr (fst ,, _)) (inl x) | zero ,, succ snd rewrite Semiring.commutative ℕSemiring snd 1 | Semiring.sumZeroRight ℕSemiring snd | fst = TotalOrder.irreflexive ℕTotalOrder x
   cantorInverseDiscrete (succ a) (b ,, zero) (inl x) (inr (fst ,, snd₁)) | zero ,, succ snd rewrite fst | Semiring.commutative ℕSemiring snd 1 | Semiring.sumZeroRight ℕSemiring snd = TotalOrder.irreflexive ℕTotalOrder x
   cantorInverseDiscrete (succ a) (b ,, succ c) (inl x) (inr (fst ,, snd1)) | zero ,, succ snd = zeroNeverGreater (canRemoveSuccFrom<N snd1)
@@ -129,14 +129,14 @@ module Sets.CantorBijection.Proofs where
     where
       bad : {a : ℕ} → 1 ≡ succ (succ a) → False
       bad ()
-  cantorInverseDiscrete (succ a) (b ,, c) (inl y) (inl x) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder y x)
+  cantorInverseDiscrete (succ a) (b ,, c) (inl y) (inl x) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder y x)
   cantorInverseDiscrete (succ a) (b ,, c) (inr (bad ,, _)) (inl x) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x bad)
   cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inr (bad ,, snd)) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x bad)
   cantorInverseDiscrete (succ a) (b ,, c) (inr (_ ,, bad)) (inr (fst₁ ,, snd)) | succ (succ fst) ,, zero rewrite Semiring.commutative ℕSemiring fst 2 | Semiring.commutative ℕSemiring fst 1 = noIntegersBetweenXAndSuccX 1 bad snd
   cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inl y) | succ zero ,, succ snd rewrite Semiring.sumZeroRight ℕSemiring snd = noIntegersBetweenXAndSuccX (succ (succ snd)) x y
   cantorInverseDiscrete (succ a) (zero ,, c) (inr (fst ,, snd1)) (inl y) | succ zero ,, succ snd rewrite Semiring.sumZeroRight ℕSemiring snd = noIntegersBetweenXAndSuccX (succ (succ snd)) snd1 y
-  cantorInverseDiscrete (succ a) (succ b ,, c) (inr (fst ,, bad)) (inl y) | succ zero ,, succ snd rewrite Semiring.sumZeroRight ℕSemiring snd | fst = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder bad (identityOfIndiscernablesRight _<N_ (addingIncreases c b) (Semiring.commutative ℕSemiring c (succ b))))
-  cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inl y) | succ (succ fst) ,, succ snd rewrite Semiring.commutative ℕSemiring fst (succ (succ (succ snd))) | Semiring.commutative ℕSemiring (succ (succ snd)) fst = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder y x)
+  cantorInverseDiscrete (succ a) (succ b ,, c) (inr (fst ,, bad)) (inl y) | succ zero ,, succ snd rewrite Semiring.sumZeroRight ℕSemiring snd | fst = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder bad (identityOfIndiscernablesRight _<N_ (addingIncreases c b) (Semiring.commutative ℕSemiring c (succ b))))
+  cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inl y) | succ (succ fst) ,, succ snd rewrite Semiring.commutative ℕSemiring fst (succ (succ (succ snd))) | Semiring.commutative ℕSemiring (succ (succ snd)) fst = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder y x)
   cantorInverseDiscrete (succ a) (b ,, c) (inl x) (inr (y ,, z)) | succ (succ fst) ,, succ snd rewrite y | Semiring.commutative ℕSemiring fst (succ (succ (succ snd))) | Semiring.commutative ℕSemiring (succ (succ snd)) fst = TotalOrder.irreflexive ℕTotalOrder x
   cantorInverseDiscrete (succ a) (b ,, c) (inr (x ,, y)) (inl z) | succ (succ fst) ,, succ snd rewrite equalityCommutative x | Semiring.commutative ℕSemiring fst (succ (succ (succ snd))) | Semiring.commutative ℕSemiring (succ (succ snd)) fst = TotalOrder.irreflexive ℕTotalOrder z
   cantorInverseDiscrete (succ a) (b ,, c) (inr (x ,, y)) (inr (m ,, n)) | succ (succ fst) ,, succ snd = noIntegersBetweenXAndSuccX (succ (succ snd)) y n